形式化方法在电信服务系统中的应用与研究

为提高电信服务系统的稳定性．把形式化方法引入到电信服务系统的研究中,并用典型的形式化规格语言Z开发电信系统中基本功能的形式化规格,该套形式化规格对拔打电话、建立连接、释放连接、修改密码等操作的进行详细、精确的描述。基于Z语言的形式化规格可以应用于电信服务系统开发过程的各个阶段．以期减少电信服务系统内部错误的产生、提高稳定性。     

从类树形流程图到Z语言的形式化规格

在软件工程中,使用Z语言形式化规格可以大大提高软件开发质量,提高稳定性,降低开发成本,但要开发出高质量的形式化规格并通过验证,却需要损耗较多的时间和精力.为使软件开发人员能够较快地并且高质量地开发出基于Z语言的形式化规格,提出一种简明的类树形流程图,并以电信服务系统中的呼叫转移功能模块为例子,详细描述如何把类树形流程图应用到Z语言的形式化规格开发当中,以期为开发人员带来便利,节省开发时间,提高形式化规格的质量.     

一种入侵检测系统的形式化建模及其检测方法的研究

在入侵检测系统的开发过程中应用形式化的规格说明方法，可保证所开发的系统能够满足系统的安全需求，增强用户对所实现系统的信任。以Z方法对所设计的分布式拒绝服务(DDoS)入侵检测系统进行规格说明为例，将Z的应用扩展到安全关键系统的开发和设计领域。     

Z规格说明自动生成器

形式化Z语言采用严格的数学理论可以有效提高软件的可靠性和鲁棒性,但是由于其包含的数学理论使得只有少数人能够熟练应用Z语言进行形式化规格说明书的编写.目前,多数对于Z语言的研究集中在理论阶段,还没有相应的工具支持Z规格说明的自动生成.本文中对于Z规格说明自动生成器的研究有助于降低Z规格说明书的编写难度,降低了形式化开发的难度及成本,对于形式化Z语言的推广具有重要的意义.     

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

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

答疑系统问题的Z语言规约

分析了目前答疑系统存在的不足之一,即缺少标准框架,从而很难实现答疑系统之间资源的共享.因此提出了使用形式化方法来构建统一的答疑系统,利用形式化语言Z对答疑系统的主要模块进行需求规格说明.同时用Z语言描述了答疑系统的主要操作模式,包括关键词的提取、问题的检索和知识库的更新等操作.     

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

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

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

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

Z的面向对象扩充COOZ的设计

为了使Z规格说明与面向对象开发方法相结合，本文在Z中扩充了对象类型和模块描述机制，使之成为面向对象的形式化规格说明语言COOZ（completeobject－orientedZ）．内容包括COOZ的设计思想、语法定义及说明、形式化语义、实例以及与相关研究工作的比较．     

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

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

一种在Internet环境下提交与发布Z规格说明的方法

用形式方法开发软件可提高软件系统的正确性和可靠性，并可提高软件开发的效率。Z是一种基于状态的形式规格说明语言。但是一直以来形式方法在工业上不能得到普遍的应用，一个原因是它缺乏有效的支持工具以及向通用的工业标准转化的连接。本文首先用JAVA语言和XML开发了一种方法，使得用户能够在不同的平台上、不同的浏览器上利用GUI的方式编辑Z规格说明，进而转化成服务器端的以XML方式描述的Z模式。通过XSL所定义的格式，又将以XML方式描述的Z发布到网页上。从而实现了Z规格说明在WWW环境下的共享与发布。     

基于Object—Z的形式化验证方法

定理证明是一种形式化验证技术，也是形式化方法的重要组成部分，它能从形式规格说明中推理出应具备的性质与属性，从而可以对规格说明进行形式验证。Obiect-Z是形式规格说明语言Z的面向对象扩充，基于集合论与数理逻辑，具有严密的逻辑性，适合精确地描述大型软件系统，并且可以对其形式规格说明进行推理。本文首先给出了基于Object—Z规格说明的定理证明验证方法，接着用Object-Z描述了一个电梯操作系统的实例，在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。     

Towards the formal specification of an OPS5 production system architecture

The article presents a formal specification for many important aspects of the OPS5 production systems framework. the article illustrates how an abstract formal specification of a production system can be created and the benefits this provides to those involved in the development of knowledge-based systems. the formal specification is preceded by an informal specification of a production system upon which the formal model is based and the development is illustrated through the use of concrete examples. the notation used is that of “Z” (J. M. Spivey, The Z Notation, Prentice-Hall, Englewood Cliffs, NJ, 1990), a language based upon typed set theory. This language has been used to success in the specification of critical conventional software systems (I. Hayes, Technical Monograph PRG-46, Oxford University Computing Laboratory, Oxford, England, 1985) and which is formal enough to allow for the creation of rigorous specifications, yet is of a form that makes these specifications “readable.” the aim of the article is to show that formal techniques can be applied to areas of knowledge-based system development, thus promoting correctness, reliability, and understanding. © 1994 John Wiley & Sons, Inc.     

一个Object-Z规格说明的证明责任产生器

定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合于精确地描述大型软件系统,并且可以对其形式规格说明进行推理。设计一个证明责任产生器,从Object-Z形式规格说明出发,按照相关规则自动抽取相应的证明责任,这些证明责任可以直接输入到已有的定理证明器Z/EVES中进行证明之。证明责任产生器起着Object-Z规格说明编辑器与证明器Z/EVES之间的桥梁作用,方便于Object-Z形式规格说明的验证。     

A decomposition of a formal specification: an improvedconstraint-oriented method

In this paper, the authors propose a decomposition method for a formal specification that divides the specification into two subspecifications composed by a parallel operator. To make these specification behaviors equivalent before and after decomposition, the method automatically synthesizes an additional control specification, which contains the synchronization information of the decomposed subspecifications. The authors prove that a parallel composition of the decomposed subspecifications synchronized with the control specification is strongly equivalent with the original (monolithic) specification. The authors also write formal specifications of the OSI application layer's association-control service and decompose it using their method as an example of decomposition of a practical specification. Their decomposition method can be applied to top-down system development based on stepwise refinement     

Specifying a safety-critical control system in Z

The paper presents a formal specification in the Z notation for a safety-critical control system. It describes a particular medical device but is quite generic and should be widely applicable. The specification emphasizes safety interlocking and other discontinuous features that are not considered in classical control theory. A method for calculating interlock conditions for particular operations from system safety assertions is proposed; it is similar to ordinary Z precondition calculation, but usually results in stronger preconditions. The specification is presented as a partially complete framework that can be edited and filled in with the specific features of a particular control system. Our system is large but the specification is concise. It is built up from components, subsystems, conditions and modes that are developed separately, but also accounts for behaviors that emerge at the system level. The specification illustrates several useful idioms of the Z notation, and demonstrates that an object-oriented specification style can be expressed in ordinary Z     

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.