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

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

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

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

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

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

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

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

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

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

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

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

基于问题模式的形式化软件规格说明生成方法

精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明.     

Object-Z 规格说明测试用例的自动生成器

对Object-Z形式规格说明构造测试用例的研究,目前主要集中在理论研究阶段,测试用例的自动生成几乎没有相应的工具支持.Object-Z是基于数学和逻辑的语言,并大量使用了模式复合和简写形式,这给计算机提取完整语义用以自动产生测试用例造成了困难.通过展开Object-Z规格说明中的模式定义,改进Object-Z的文法结构,给出了提取Object-Z规格说明语义的方法,研究了从Object-Z规格说明产生测试用例的自动化过程.这一过程主要包含3个阶段:Object-Z语言的自动解析、语义自动抽取和测试用例自动产生.通过介绍的工具原型,可以很容易得到规格说明中的各种语义;基于某些测试准则,能够方便自动产生可视化的抽象测试用例.     

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

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

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

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

Z状态空间和操作定义的自动生成技术

从软件需求定义到形式功能堆约的自动转换是需求工程的重要问题之一。文中以软件需求定义语言ＮＤＲＤＬ和形式功能规给语言Ｚ为基础，探讨了基间的自动转换技术，特别是从ＮＤＲＤＬ需求定义自动获取Ｚ形式规约中状态空间与操作定义的技术。     

OOZE求精技术自动化的探讨

文中立足于一种Ｚ的面向对象扩充广谱语言ＯＯＺＥ，研究其从软件规格说明到可执行程序求精过程的自动化技术，重点讨论了数据求精技术，对Ｚ中的几种复合数据类型及其嵌套结构，ＯＯＺＥ中的类结构提出了相应的自动求精规则，同时给出了采用自动化技术进行操作求精的一般步骤。     

基于动作推导引擎下的故障检测方法

本文根据文[2]介绍的软件管理者方法，提出了基于动作推导引擎的软件管理者方法。软件管理者单元是一种自动的实时监控软件故障的软件工具，适用于实时软件系统特别是通信类软件系统的故障侦测。它通过监控目标系统的输入和输出，使用获得的输入和目标系统的管理模型推算出对应此输入序列的期望输出值．与目标系统的实际输出做比较．如果实际输出没有在期望输出集中，则管理者单元断定目标系统出现错误。基于动作推导引擎的软件管理者方法，采用了动作推导引擎产生的目标系统管理模型，使该管理模型独立于软件管理者方法。可以实现管理模块与动作推导引擎同步实时更新．而不会导致软件管理者单元的改动。     

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

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

从过程描述语言到Z语言

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

关于功能模拟器生成环境的研究

为了满足专用指令集处理器的发展和产品上市时间缩短的需要，功能模拟器的自动生成方法受到越来越多的关注。该文介绍了一种体系结构描述语言xpADL驱动的模拟器生成环境，它由xpADL、模拟器生成器和函数库三部分组成。XpADL对目标体系结构的行为和组成进行描述。然后牛成器对描述文件进行解析。将其转化为树型抽象表示并生成相应的体系结构相关部分，这部分和函数库组成了功能模拟器。在实验部分，通过StrongArm和PISA两种．体系结构的功能模拟器的自动生成，证明了方法的正确性和有效性。该文的研究结果对于嵌入式系统的设计具有重要的指导意义。     

一种基于Z规范的纯函数式程序设计方法

状态、输入和输出是Z规范的基础,引入Monad的纯函数式语言特别适合用来实现用Z规范说明的系统.通过将状态、输入和输出封装在一个Monad内,提出一种基于Z规范的纯函数式程序设计方法.