基于Event-B的航天器内存管理系统形式化验证

内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会较之前的验证工作带来更多难题,主要体现在：内存管理模块中的复杂数据结构的形式化描述;操作的规范语义;行为的建模;内部函数的规范及断言定义与循环不变式的定义;实时性验证等方面.本文拟针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法,来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.本文研究成果有望被直接应用于我国新一代的航天器系统上.     

一种顺序图的形式化描述与推理过程

以统一建模语言(UML,Unified Modeling Language)规范为基础,给出UML顺序图的形式化定义和语法描述,并进一步分析了对象消息发送和接收之间的一致性问题.最后,通过对实例推理过程的分析,对UML顺序图的特性作进一步的解释.这为基于UML顺序图的模型转换和模型验证提供了必要的前提条件,可用于对软件...     

基于模型转换的MARTE顺序图的形式化分析

作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TrS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时阃变迁系统(TrS)扩充成TrS4SD,用TrS4SD描述顺序图的形式语义,最后对TrS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TrS4SD的转化过程以及基于TTS4SD的验证方法.     

支持业务事务验证的服务协调模型

在Web服务业务流程中如何保证参与者之间的协调一致性是亟待解决的重要问题.Web服务事务规范中描述的参与者之间的交互消息缺乏严格的语义,无法精确地描述复杂的协调活动,本文用Pi-演算形式化描述WS -TX规范中定义业务活动事务的WS-BA协议,在此基础上建立了适用于多方参与的业务事务的服务协调模型;并利用基于等价自动机转换的HAL模型检测工具,验证分析了WS-BA协议的安全性和活性,给出一个多方参与的业务事务实例的验证过程,介绍如何利用模型检测技术来分析业务流程设计正确性的方法,有效地确保了业务事务执行的可靠性和一致性.     

一种用户身份认证系统的形式化描述

身份认证系统用于解决访问者的物理身份和数字身份的一致性问题,给其他系统提供权限管理的依据.运用形式化方法,针对一个用户身份认证系统,使用Z语言对其进行形式化描述.在形式化过程中,对该系统用户身份记录定义了读、添加、更新、删除四种操作,对该系统用户身份认证定义了登录、退出二种操作.对于每种操作,还定义了具体的操作步骤、操作需要的前提条件和提示信息.身份认证是整个信息安全体系的基础,并越来越受到重视,因此研究身份认证系统的形式化具有一定的现实意义.     

基于UML的嵌入式建模方法改进策略研究

统一建模语言UML(unified modeling language)在嵌入式系统设计建模中已经获得了广泛的承认,有很多成功的应用.但UML在嵌入式建模中存在时间约束描述能力不强和所建模型形式化复杂、验证难及模型重用性不高等问题.针对这些问题提出了一种改进策略:定义实时语义和映射规则,建立实时描述模式模板,使用模板中实时描述模式描述时间约束信息.改进后的方法能可视化地分析模型、纠正错误和简单地进行形式化转换,能利用支撑工具对模型进行验证,较好地解决了UML在嵌入式系统建模中存在的问题.     

指挥控制协同能力需求体系形式化框架

指挥控制协同性是实现信息化条件下联合作战指挥的关键。针对当前对指挥控制协同能力需求缺乏形式化描述和分析方法等问题,提出一种指挥控制协同能力需求形式化描述框架,运用进程代数方法对能力之间的关系以及操作进行形式化定义,消除了采用自然语言描述协同能力合成过程中可能产生的语义二义性。案例分析验证了该方法的可用性和有效性。     

复杂内核数据结构程序形式化验证

操作系统内核作为软件系统的基础组件, 其安全可靠是构造高可信软件系统的重要环节, 但是, 在实际的验证工作中, 操作系统内核中全局性质的不变式定义, 复杂数据结构程序的形式化描述和验证仍存在很多困难. 本文针对操作系统内核中满足的全局性质, 在代码层以函数为单位, 用全局不变式进行定义, 并在不同的函数中进行形式化验证, 从而证明各个函数符合操作系统内核的全局性质; 针对操作系统内核中经常使用的复杂数据结构程序, 本文通过扩展形状图理论, 提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序, 并对该方法进行了正确性证明, 最终成功验证操作系统内核中关于任务创建与调度, 消息队列创建与操作相关的代码.     

扩展不干扰模型(ENISM)及基于CSP的描述和验证方法

在不干扰理论的基础上,提出扩展不干扰模型ENISM及其验证方法,用以描述和分析操作系统中的信息流策略.工作包括:(1)依据系统功能模块定义多个执行域,以即将执行的可能动作序列集合与可读取的数据存储值集合一同作为ENISM定义执行域安全状态的基础;(2)给出判定系统中不存在违反策略的执行轨迹和数据流动的条件ENISM-CC;(3)基于通信顺序进程给出ENISM-CC的语义及操作系统模块设计的形式化描述和验证方法.     

基于自动机的构件实时交互行为的形式化模型

采用形式化方法对复杂实时构件系统交互行为进行描述和验证,对于提高系统的正确性、可靠性等可信性质具有重要意义.分析了基于进程代数和自动机的构件交互行为形式化建模方法各自的优缺点,在此基础上提出了基于时间构件交互自动机的建模方法,给出了时间构件交互自动机的相关定义、组合和验证算法.时间构件交互自动机引入了时间限制、时间代价、时间代价计算半环、构件组合层次等概念,既能够描述构件交互情况,又能够清楚地表示出构件系统的体系结构信息和实时信息,便于对系统进行描述和验证.最后,结合具体应用给出了应用示例.     

基于Z规格的UML模型形式化转换及验证

统一建模语言(UML)所建立的模型的正确性无法通过其本身进行形式化验证,为解决这个问题,根据UML模型的静态性质和动态模块行为两个方面提出结合形式化规格说明语言的模型形式化方案,以此为基础提出将UML目标模型转化为Z规格说明的形式化方法,并用Z-EVES工具形式化检测Z规格描述的正确性.通过实例分析验证了该方法的可行性.     

Methodical specification of abstract data types via rewriting systems

A data type is often given by an informal model. Its formal specification is an important task, but also difficult and error-prone. Here a methodology for this task is presented. Its steps are, first, the election of a canonical form defining a canonical term algebra; second, a system of sound rewriting rules powerful enough to achieve the syntactical transformations of the canonical term algebra. The final translation of rewriting rules into equations is immediate. The methodology is illustrated by the detailed presentation of a simple example.Research partly sponsored by FINEP, CNPq and the French Ministry for Foreign Affairs.     

多态性构件及其代数规范

可复用构件往往需要引入多态性支持,但是这给构件的形式化定义带来很多困难.采用代教规范系统来定义空间几何实体构件的组织结构及其行为特征,可以有效的支持构件的数据和行为多态性.在多层次的代数规范理论基础上,引入了构件的参数化多态和包含多态,建立了空间几何的实体多态性构件系统,实例表明了系统对于数据和行为多态性方面的有效性.     

基于形式化规格说明的UML状态图提取

为了辅助软件开发者理解形式化规格说明,提出一种从B方法规格说明中提取UML状态图的方法。通过分析状态信息在规格说明中的表现形式,定义一系列精确的简单状态、状态迁移、复合迁移、分层状态和状态图通信等提取规则。借助状态变量表和状态迁移表,最终实现状态元素和状态关系的提取,并以此构造完整的UML状态图。实验结果验证了方法的正确性及有效性。     

VLSI asynchronous systems: specification and synthesis

Most of today's digital systems are realized using synchronous (i.e. globally clocked) VLSI circuits. For many reasons, it is becoming increasingly hard to build large synchronous circuits. Although several techniques for building non-clocked (i.e. asynchronous) sequential circuits have been known for some time, they have been largely ignored by the digital design community. Recently, however, asynchronous circuits have been enjoying a revival. After reviewing recent research in this area, we take a simple collection of examples and, through them, explain our design system for specifying and synthesizing asynchronous circuits. We show that by being able to work in a framework where circuit activities do not have to coincide with clock pulses, designers obtain several avenues for circuit optimization that are highly promising for creating efficient and modularly expandable circuits.     

PAR平台从规约出发的算法推导与自动生成

简要介绍PAR方法及其支撑平台,使用PAR方法及其平台从规约出发形式化推导并生成了两个典型的算法程序。PAR方法及其平台使用一阶谓词逻辑表示功能规约,分划与递推来进行算法形式推导,各种转换系统来自动生成算法程序。这显著地提高了算法程序的正确性和开发效率,也有助于深刻地理解算法设计思想。     

Towards formal specification of a distributed computing system

Onboard spacecraft computing system is a case of a functionally distributed system that requires continuous interaction among the nodes to control the operations at different nodes. A simple and reliable protocol is desired for such an application. This paper discusses a formal approach to specify the computing system with respect to some important issues encountered in the design and development of a protocol for the onboard distributed system. The issues considered in this paper are concurrency, exclusiveness and sequencing relationships among the various processes at different nodes. A 6-tuple model is developed for the precise specification of the system. The model also enables us to check the consistency of specification and deadlock caused due to improper specification. An example is given to illustrate the use of the proposed methodology for a typical spacecraft configuration. Although the theory is motivated by a specific application the same may be applied to other distributed computing system such as those encountered in process control industries, power plant control and other similar environments.     

Formal specification – an analytic tool for (management) information systems

Abstract. There appears to be a general consensus within the information systems literature that formal specification of software systems is an inappropriate response to the perceived general failure of information systems to meet user requirements. Such views would seem to be based primarily on the difficulty of constructing formal specifications – and on the difficulty of understanding such specifications once constructed. Research into the applicability of formal methods has therefore tended to concentrate on the needs and the context of software developers specializing in critical and extremely complex software such as operating systems, transaction processing monitors, or nuclear reactor protection. More recently, however, formal methods have been applied successfully in more conventional and commercial areas, such as the development of a CASE tool, indicating that many of the perceived disadvantages of formal methods are merely myths.
This paper discusses the differing research directions of the information systems and software engineering disciplines and suggests that significant beneflts may result from a synthesis of the two approaches. We further suggest that there is a serious danger that approaches which have been shown to have value in one of the two domains are automatically being ignored in the other as being 'irrelevant'. While each of the two areas ignores the contribution of the other, software systems will continue to be sub-optimal (in terms of relevance, as well as quality). We argue the relevance of formal specifications to the information systems discipline, illustrating the argument with a case study based within the IS domain.     

Program Constructionby Verifying Specification

A program construction method based on Gamma language is proposed.The problem to be solved is specified by first-order predicate logic and a semantic verification program is constructed directly from the specification.Ways for improving efficiency of the program are also studied.The method differs from the one proposed by Manna and Waldinger,where a program is extracted from the proof of the existence of an object meeting the given specification.On the other hand,it also differs from the classical one used for deriving Gamma programs of Banatre and Le metayes,which consists in decomposing the specification into an invariant and a termination conditon.