基于Z语言的电信服务系统的形式化规格

形式化方法是基于数学的系统开发方法,它可以应用于系统开发的各个阶段,包括系统需求、设计、实现、测试等。首先介绍了形式化规格语言Z,接着用Z开发电信服务系统的形式化规格,并对形式化规格进行验证,以期提高电信服务系统的稳定性,也为探测电信服务系统的功能冲突、预防系统缺陷的产生提供研究的基础和支持。     

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

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

Z规格说明自动生成器

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

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

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

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

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

安全应用系统的形式化规范与求精过程研究

形式化方法是提高系统安全等级必不可少的保障技术。然而,由于诸多原因,它在安全应用系统开发过程中的应用尚不普及。本文将以Z语言为依托,以Mondex电子钱包系统为范例,探讨形式化方法在安全应用系统开发过程中的应用方法和过程。     

Z语言检测出的电信系统的故障类型总结

电信系统的复杂性致使其故障较难检测,形式化规格语言Z对检测电信系统的故障具备较好的优势。在结合之前研究成果的基础上,对Z语言检测出的电信系统的故障类型进行详细的总结,这些故障类型都具备较强的隐蔽性,证明Z语言对提高软件开发的质量能起到很好的效果。对电信系统故障的解决方法提出建议．以期提高电信系统的软件质量和稳定性。     

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

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

B语言和方法与Z、VDM的比较

1 引言形式化方法是建立在严格数学基础上的软件开发方法。软件开发的全过程中,从需求分析、规格说明、设计、编程、系统集成、测试、文档生成直至维护各阶段,凡是采用严格的数学语言、具有精确的数学语义的方法都称为形式化方法。形式化方法的一个重要研究内容是形式规格说明,即用具有精确语义的形式化语言书写的程序功能描述,它是论证程序是否正确的依据。形式化方法需要形式规格说明语言的支持,也可以说形式化方法的关键在于形式规格说明语言。形式规格说明语言提供了一个称为语法域的记号系统和一个称为语义域的目标集合,以及一组精确地定义哪些目标系统满足哪个规格说明的规则。根据对目标软件系统进行说明的方式分三种规格说明语言:     

面向服务的软件体系结构的形式化

用形式规格说明语言Z对面向服务这样一种新出现的分布式软件体系结构进行形式化，克服了原先面向服务体系结构的非形式化描述中的限制，为更好地进行面向服务的分布式软件开发提供了指导模型。     

两种形式语言:RSL与Z的分析比较

RSL(RAISE规格说明语言)和Z是目前广泛应用的软件规格说明语言,本文从软件开发生命周期的角度对两种语言进行了比较,提出了将不同规格说明语言结合形式地描述系统的设想。     

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

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

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

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

Formal specification and testing: A case study

Z is a formal notation for writing system specifications that has been growing in popularity over recent years. This paper examines some of the issues involved in applying a ‘partition based’ testing method to a system specified in Z. Details of an extensive case study are given, from specification and implementation of the system to the development and execution of test cases. The strategy is found to have benefits compared to those based on less formal specifications, but there are limitations to the approach, and difficulties that need addressing.     

Object-Z: A specification language advocated for the description of standards

The importance of formalising the specification of standards has been recognised for a number of years. This paper advocates the use of the formal specification language Object-Z in the definition of standards. Object-Z is an extension to the Z language specifically to facilitate specification in an object-oriented style. First, the syntax and semantics of Object-Z are described informally. Then the use of Object-Z in formalising standards is demonstrated by presenting a case study based on the ODP Trader. Finally, a formal semantics is introduced that suggests an approach to the standardisation of Object-Z itself. Because standards are typically large complex systems, the extra structuring afforded by the Object-Z class construct and operation expressions enables the various hierarchical relationships and the communication between objects in a system to be succinctly specified.