面向方面的实时系统形式化开发方法

实时系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要如面向方面和基于组件的软件工程方法的支持,同时实时系统的可信性要求采用形式化方法来开发实时系统。本文试图建立一种面向方面的实时系统形式化开发方法,这种方法对RT—Z进行了面向方面和面向部件的扩展,并通过实时组件模型在需求和设计阶段提供了对基于部件的系统开发方法(CBSD)和面向方面的系统开发方法(AOSD)的支持。本文给出了面向方面的实时Z(AO—RT—Z)的组件模型的框架结构、语法要求、方面的联结和功能接口和非功能接口的定义,重点讨论并证明了面向方面的实时Z(AO—RT—Z)作为规格描述语言的健全性。     

从过程描述语言到Z语言

Z语言是一种得到广泛应用的形式化规格语言，Z语言可以方便地描述系统操作的数据转换，却很难描述系统操作间的时序关系，而过程描述语言可以方便地描述时序关系，本文利用时序状态转换系统作为中介，提出一种把过程描述语言的项转换成Z规格的机械算法，利用这一算法，Z文也能方便地描述时序关系，本文还通过实例说明了该算法在多视点需求工程中的应用。     

基于实时语言和面向方面的形式化开发方法

面向方面方法和实时语言特性应用于实时软件开发工程，将降低实时软件开发的复杂性，而形式化方法将提升系统的可信度。该文提出的一种面向方面的实时软件开发方法AOSDBRTL，它基于经面向方面扩展的形式化方法AO RT Z，在编码阶段应用实时语言PEARL，实现了软件开发各个阶段对面向方面的无缝支持。     

基于时序Petri网的联锁逻辑形式建模与验证

时序Petri网结合Petri和时序逻辑的优点,清晰简洁地描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性。文章给出安全苛求系统——车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的。     

基于状态转换系统的Z语义模型扩充

利用状态转换系统对Z语义模型进行分析。指出其三种不足；然后利用状态转换系统、有限状态转换系统和时序状态转换系统。对Z语义模型分别进行多样性、有效性和时序性扩充，定义多种数据实现关系和时序实现关系，导出相应的求精关系；并通过一个简单的实例说明Z语义模型扩充在多视点需求工程中的应用．     

基于UML-RT的复杂嵌入式系统建模方法及其应用

分析了UML在实时系统设计中的优点和需要解决的主要问题,论述了基于UML RT的实时嵌入式系统设计方法,并且对其进行扩展以支持数据流计算模型的建模,最后以汽车巡航系统为例加以说明。     

公平转换系统规范及其应用*

本文讨论了用于并发系统规范的2种方法；时序逻辑方法和状态自动机方法．由此，本文提出了一种新的规范形式——公平转换系统规范FTSS(fair transition system specification)．此规范方法集成了状态自动机方法和时序逻辑方法的优点，改进了时序逻辑方法通常较复杂、不易理解，特别是它不能用于描述并发系统的局部性质等不足．进一步对FTSS中的每一部分进行了讨论，得到结论；FTSS是机器封闭的，规范过程是相容的且是完全的．一个有丢失传输协议的例子表明作者的方法具有简单、直观、易于理解和便于使用等特点．最后给出了FTSS的一些应用．它为程序验证和并发系统的逐步求精提供了一个统一的框架，已成功地应用于程序验证中．     

公平转移系统规范及其应用

本文讨论了用于并发系统规范的２种方法：时序逻辑方法和状态自动机方法，由此，本文提出了一析的规范形式－－公平转换系统规范ＦＴＳＳ（ｆａｉｒ ｔｒａｎｓｉｔｉｏｎ ｓｙｓｔｅｍ ｓｐｅｃｉｆｉｃａｔｉｏｎ），此规范方法集成了状态自动要方法和时序逻辑方法的优点，改进 时序逻辑方法通常较复杂，不易理解，特别唱它不能用于描述并发系统的局限性质等不足，进一步对ＦＴＳＳ中第一部分进行了讨论，是到结论，ＦＴＳＳ是     

入侵特征的时间语义分析及实现

入侵特征对于入侵检测系统至关重要，它们往往由系统属性和事件序列组成，时序关系是描述它们的关键。ISITL(Intrusion Signatures based on Interval Temporal Logic)是一种较高抽象程度的入侵特征形式化描述语言，它对Allen的时段时态逻辑进行了实时描述的扩充，从而加强了其入侵特征的描述能力。在ISITL中，所有的系统属性和事件都与相应的时段紧密相连，其相互关系用13个基本函数和3个扩展函数来描述。与其它入侵特征描述语言相比，ISITL具有简单易用，描述能力强等优点。     

集成功能块和UML－RT的功能块适配器研究

分布式工业过程测量和控制系统常以功能块来构建,而利用UML－RT建模又便于实时控制系统的扩展,这要求集成UML－RT组件和功能块,实现UML－RT协议到功能块协议的映射。研究了用于连接UML－RT封装体和IEC61499功能块的模型元件：功能块适配器,它提供了同UML－RT封装体和功能块相交互的接口。描述了功能块适配器的概念、结构及接口,说明了功能块适配器的执行模型。     

An Overview of the Integrated Formalism RT-Z

We present an integration of the formal specification languages Z and timed CSP, called RT-Z, incorporating their combined strengths in a coherent frame. To cope with complex systems, RT-Z is equipped with structuring constructs built on top of the integration, because both Z and timed CSP lack appropriate facilities. The formal semantics of RT-Z, based on the denotational semantics of Z and timed CSP, is a prerequisite for preciseness and mathematical rigour. RT-Z is intended to be used in the requirements definition and design phases of the system and software development process. The envisaged application area is the development of real-time embedded systems. Received September 2000 / Accepted in revised form June 2001     

形式化语言RT-Z的合成及其应用

Z是一种确定相关数据特征的非常成功的形式化语言，却在构造动态行为方面的模型缺乏相应的功能；而Timed CSP是一种确定动态行为的功能强大的语言，但它没提供适当的结构来构造相关数据特征。文中通过形式化语言Z和过程代数Timed CSP合成一种新的形式化方法RT-Z，使得RT-Z在软件系统开发过程的需求定义和设计阶段能书写软件系统一致、简单的规格说明。     

A refinement-based process algebra for timed automata

We propose a real-time extension to the process algebra CSP. Inspired by timed automata, a very successful formalism for the specification and verification of real-time systems, we handle real time by means of clocks, i.e. real-valued variables that increase at the same rate as time. This differs from the conventional approach based on timed transitions. We give a discrete trace and failures semantics to our language and define the resulting refinement relations. One advantage of our proposal is that it is possible to automatically verify refinement relations between processes. We demonstrate how this can be achieved and under which conditions.Partially supported by EPSRC grant GR/N22960.Received January 2004Revised September 2004Accepted December 2004 by M. Leuschel and D. J. Cooke     

A theory of Orwellian specifications with NewThink

We introduce NewThink, a specification language designed specifically for real-time safety-critical systems. NewThink is a component of an overall Orwellian development method for safety-critical systems which consists of a specification language, a programming language and a set of sound decomposition rules. In this paper, we present the syntax and semantics of NewThink. We demonstrate a relationship between timed and static specifications, which potentially allows us to continue using techniques from the static case in the timed case. We also prove that our extension for real-time is conservative, which is very much in keeping with our Orwellian philosophy.     

一种从Object—Z到CSP规格说明的转化方法

面向对象形式规格说明语言Object-Z与进程代数CSP相结合是当今的一个热点,它既可以表示复杂的模块化数据与算法,又可以表示系统的行为,但求精与验证对它们结合后的规格说明需要分别进行处理。本文提出了一个方法,把Object-Z规格说明转化为CSP规格说明,可以方便地处理结合后的规格说明,因此求精与推理对结合后的规格说明可以按CSP规则与方法一致来进行处理。此外,转化后的Object-Z规格说明可以按照CSP方法进行模型检查。     

Object modelling and formal specification during real-time system development

Object oriented techniques promote understanding of requirements leading to flexible and extendible designs. The use of formal specification techniques ensures a complete understanding of system requirements and provides sound foundations for subsequent testing and verification. This paper describes the use of the Z and Timed CSP formal specification techniques to support object modelling during real-time system development. Relationships between class attributes are specified within the corresponding Z schemas and inheritance relationships between classes are formally specified using the schema extension mechanism of Z. Z is used to specify the domain types of the attributes of classes identified during object oriented analysis and design. Z is also used to produce model based specifications of the methods within classes that are specified informally during functional analysis. Dynamic analysis identifies events, states and temporal relationships between events. Timed CSP is used to formally specify this information as well as timing information that is necessary during real-time system development.     

A process algebraic framework for specification and validation of real-time systems

Following the trend to combine techniques to cover several facets of the development of modern systems, an integration of Z and CSP, called Circus, has been proposed as a refinement language; its relational model, based on the unifying theories of programming (UTP), justifies refinement in the context of both Z and CSP. In this paper, we introduce Circus Time, a timed extension of Circus, and present a new UTP time theory, which we use to give semantics to Circus Time and to validate some of its laws. In addition, we provide a framework for validation of timed programs based on FDR, the CSP model-checker. In this technique, a syntactic transformation strategy is used to split a timed program into two parallel components: an untimed program that uses timer events, and a collection of timers. We show that, with the timer events, it is possible to reason about time properties in the untimed language, and so, using FDR. Soundness is established using a Galois connection between the untimed UTP theory of Circus (and CSP) and our time theory.     

用带时钟变量的线性时态逻辑扩充Object-Z*

Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首先用时钟变量扩充线性时态逻辑,接着提出了一个方法——用带时钟变量的时态逻辑(LTLC)来扩充Object-Z。用LTLC扩充的Object-Z是一个模块化规格说明语言,是Object-Z语法和语义的最小扩充,其最大优点在于它能方便地描述和验证复杂的实时软件规格说明。