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

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

Z实时扩展及基于多视点的应用模式

RT—Z是由Z和经实时扩展的通信顺序进程timed CSP集成的用以描述实时系统的规格说明语言,它将Z对状态描述的优点和timed CsP对时序关系和并发描述的优点相结合,具有强大的描述能力;而基于时序转化系统的Z扩展适合描述系统状态的转化。给出了Z实时扩展的分类原则并从讨论了其应用特点,最后在分析RT—Z的语义集成的基础上提出了Z实时扩展的多视点应用模式。     

Unifying classes and processes

Previously, we presented Circus, an integration of Z, CSP, and Morgan’s refinement calculus, with a semantics based on the unifying theories of programming. Circus provides a basis for development of state-rich concurrent systems; it has a formal semantics, a refinement theory, and a development strategy. The design of Circus is our solution to combining data and behavioural specifications. Here, we further explore this issue in the context of object-oriented features. Concretely, we present an object-oriented extension of Circus called OhCircus. We present its syntax, describe its semantics, explain the formalisation of method calls, and discuss our approach to refinement.     

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.     

A Semantics for Timed MSC

Message Sequence Charts (MSC) is a graphical and textual specification language developed by ITU-T. It is widely used in telecommunication software engineering for specifying behavioral scenarios. Recently, the time concept has been introduced into MSC'2000. To support the specification and verification of real-time systems using timed MSC, we need to define its formal semantics. In this paper, we use timed lposet as a semantic model and give a formal semantics for timed MSC. We first define an event in a timed MSC as a timed lposet, then give a formal semantics for timed basic MSCs, timed MSCs with structures and high-level MSCs. In this paper, we also discuss some important issues related to timed MSC.     

基于CSP的OWL-S语义分析与建模

为了实现OWL-S过程模型正确性的自动化验证,提出了基于进程代数CSP的OWL-S过程模型的语义建模方法,建立了CSP的形式化语义模型,并利用该模型为OWL-S过程定义了形式化语义。最后以机票预订为例说明了采用CSP模型为OWL-S过程添加形式化语义的完整流程。由于该方法具备良好的数学基础,所以可以基于该方法开发出自动化验证OWL-S过程模型的工具,提高系统的安全性。     

Timed CSP在硬件高层设计中的应用

介绍了一种将TCSP语言用于硬件高层次系统设计的方法。该方法以HDL语言作为系统功能实现的核心，以TCSP语言作为系统高层次描述的外壳，从而弥补了HDL在高层形式说明和结构与实时功能表达方面的不足；同时该方法将时序与功能一体化描述，进一步丰富了硬件系统规格的内容，为复杂的硬件系统设计提供了一种可执行的规格说明方法。     

An Operational Semantics for Timed CSP

An operational semantics is defined for the language of timed CSP, in terms of two relations: an evolution relation, which describes when a process becomes another simply by allowing time to pass; and a timed transition relation, which describes when a process may become another by performing an action at a particular time. It is shown how the timed behaviours used as the basis for the denotational models of the language may be extracted from the operational semantics. Finally, the failures model for timed CSP is shown to be equivalent to may-testing and, thus, to trace congruence.     

Syntax and semantics of the compositional interchange format for hybrid systems

Different modeling formalisms for timed and hybrid systems exist, each of which addresses a specific set of problems, and has its own set of features. These formalisms and tools can be used in each stage of the embedded systems development, to verify and validate various requirements.The Compositional Interchange Format (CIF), is a formalism based on hybrid automata, which are composed using process algebraic operators. CIF aims to establish interoperability among a wide range of formalisms and tools by means of model transformations and co-simulation, which avoids the need for implementing many bilateral translators.This work presents the syntax and formal semantics of CIF. The semantics is shown to be compositional, and proven to preserve certain algebraic properties, which express our intuition about the behavior of the language operators. In addition we show how CIF operators can be combined to implement widely used constructs present in other timed and hybrid formalisms, and we illustrate the applicability of the formalism by developing several examples.Based on the formal specification of CIF, an Eclipse based simulation environment has been developed. We expect this work to serve as the basis for the formal definition of semantic preserving transformations between various languages for the specification of timed and hybrid systems.     

Modelling temporal behaviour in complex systems with Timebands

Complex real-time systems exhibit dynamic behaviours on many different time levels. To cope with the wide range of time scales and produce more dependable computer-based systems, we develop a Timebands model that can explicitly recognise a finite set of distinct time bands in which temporal properties and associated behaviours are described. In order to formalise the Timebands model, we propose a new timed model, named Timed Circus, of Circus, which is the combination of Z, CSP, and the refinement calculus in the setting of Unifying Theories of Programming. Different from most approaches such as Timed CSP, Timed Circus uses a complete lattice in the implication ordering to model the distinctive features of the Timebands model. As a result, the semantics of the Timebands model is built upon Timed Circus to guarantee soundness of each operator and maintain consistency and coordination between different time bands. By means of two small systems, we demonstrate how the Timebands model contributes to describing complex real-time systems with multiple time scales.     

Recursion induction for real-time processes

The theory of timed Communicating Sequential Processes is a mathematical approach to the design and analysis of timed distributed systems. This paper extends the language of timed CSP to include a general treatment of recursion. A semantics for mutual recursion is introduced, together with a sufficient condition for the necessary fixpoint to be unique. The resulting language has the familiar unwinding property of process algebra, and exhibits a number of useful algebraic identities. A theory of recursion induction is formulated, and a simple example is presented to illustrate its use.     

Editorial

In June 1999, the first International Workshop on Integrated Formal Methods was held at York University in the UK. The primary aim of the workshop was the combination of behavioural and state-based formalisms to yield practical solutions to industrial problems. The workshop proceedings were edited by Keijiro Araki, Andy Galloway and Kenji Taguchi and are available as “IFM99” (ISBN 1-85233-107-0, published by Springer). After the workshop, selected authors were invited to develop journal versions of their papers, incorporating further extensions, corrections and revisions. This was arranged by Andy Galloway who then passed the papers to the journal for refereeing. And here we must record our sincere thanks to Andy. Without his efforts this issue of the journal would simply not have been possible. Following reports from referees and senior colleagues from the editorial board (and the withdrawal of one submission for publication in a book) five papers were accepted for publication here. We hope that those rejected will be further revised and resubmitted; they contained good work but required further development. The common theme is, predictably, the marrying of component specification with control of the interconnecting system, and the first 4 papers all present variations on the theme of Z + CSP. Sühl adds an additional structuring mechanism to Z and CSP and targets his application area as real-time embedded systems, whereas Derrick and Boiten use Object-Z to give partial specifications (viewpoints) which are then combined using CSP. Smith and Hayes describe Real-time Object-Z, which results from the integration of Object-Z with timed traces, and Mahony and Dong investigate the necessary formal underpinning required to combine Timed CSP and Object-Z by means of a trace model. The final paper, by Gro?e-Rhode, introduces and illustrates a mechanism for checking the compatibility of different partial specifications and for coping with composite specifications in which different formalisms have been used. Whether or not this area of formal methods research merely allows us to integrate different, more ‘appropriate’, specification languages or gives rise to new hybrid languages remains to be seen. What is certain is that there are still many problems to be tackled and technology to be transferred.     

工作流建模语言XPDL到CSP进程的转化研究

针对工作流定义标准语言XPDL缺乏形式化语义,提出了将XPDL描述转化为通信顺序进程(CSP)的方法,从而可以利用进程代数CSP理论以加强对工作流模型的语义描述分析检测。通过实例分析具体说明转化方法的有效性。     

An Introduction to Real-Time Object-Z

This paper presents Real-Time Object-Z: an integration of the object-oriented, state-based specification language Object-Z with the timed trace notation of the timed refinement calculus. This integration provides a method of formally specifying and refining systems involving continuous variables and real-time constraints. The basis of the integration is a mapping of the existing Object-Z history semantics to timed traces. Received September 2000 / Accepted in revised form June 2001     

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

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

State-rich model checking

In this paper we survey the area of formal verification techniques, with emphasis on model checking due to its wide acceptance by both academia and industry. The major approaches and their characteristics are presented, together with the main problems faced while trying to apply them. With the increased complexity of systems, as well as interest in software correctness, the demand for more powerful automatic techniques is pushing the theories and tools towards integration. We discuss the state of the art in combining formal methods tools, mainly model checking with theorem proving and abstract interpretation. In particular, we present our own recent contribution on an approach to integrate model checking and theorem proving to handle state-rich systems specified using a combination of Z and CSP.     

Extending the SCR Method for Real-Time Systems

Wepropose timed SCR specifications, which are a generalizationof SCR specifications, intended to specify quantitative timingproperties of real-time systems. We extend the tabular notationof the SCR method to deal with sporadic and periodic timing constraints.We present a formal semantics for timed SCR specifications bytranslating them into timed transition systems. A shutdown systemin Korean nuclear power plants is used as a case study to illustratetimed SCR specifications.     

基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究

隔离有助于阻止信息泄露或被篡改、错误或失败被传递等.利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程CSP来定义上述隔离语义,并给出一个系统满足给定隔离策略的判定断言,以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证.以基于虚拟机的文件服务监控器为例,展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略.     

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

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

An introduction to ET-LOTOS for the description of time-sensitive systems

Enhanced Timed-LOTOS, called ET-LOTOS, is an extension of LOTOS allowing the modelling of time-sensitive system (i.e. systems whose behaviour is influenced by the passing of time). It is the basis of the timed extension of LOTOS currently developed by ISO (1995). The purpose of this paper is to present ET-LOTOS in a tutorial style and show its applicability. The detailed study of the formal semantics is addressed in another paper. A collection of small, but realistic, examples illustrates a wide variety of time-sensitive protocol mechanisms. These examples are used to introduce and justify the extensions of our language. Finally, the basics of the formal semantics are given and a comparison is made with other timed formalisms.