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

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

基于B方法的组件开发

现有的组件开发技术的规格说明是非形式化的,这导致了逻辑的非严密性和理解的歧义性,将会严重影响组件复用的效率。B方法是形式化方法之一,已经有功能强大的工具支持软件的形式化开发过程,它通过严格的数学推导和证明来保证软件设计和代码的正确性。为此,将B方法应用于学生信息管理系统的开发,提供了学生组件从需求规格说明、精化到最终实现的开发过程。通过对这一实例的研究可以看出,B方法增强了组件的规范性,对于提高组件复用的可靠性有重大的意义。     

一个抽象机库中B方法的研究

B方法是支持规格说明到软件设计和执行的形式化方法。文章研究了B方法中一种抽象机库的实现模型和生成代码,对该方法的特点进行评述。验证了B的正确可靠的实现方法,充分利用B方法的精化原则,提高了B形式化方法的开发验证效率。     

基于B方法的组件开发

现有的组件开发技术的规格说明是非形式化的，这导致了逻辑的非严密性和理解的歧义性，将会严重影响组件复用的效率。B方法是形式化方法之一，已经有功能强大的工具支持软件的形式化开发过程，它通过严格的数学推导和证明来保证软件设计和代码的正确性。为此，将B方法应用于学生信息管理系统的开发，提供了学生组件从需求规格说明、精化到最终实现的开发过程。通过对这一实例的研究可以看出，B方法增强了组件的规范性，对于提高组件复用的可靠性有重大的意义。     

B方法规格说明的构造及应用

B方法是一种软件形式化方法,支持从规格说明到代码生成的整个软件开发周期.本文比较系统地分析了B方法规格说明的构造结构,并结合所设计的实例演示了用B方法编写规格说明的过程,简略地给出了其规格说明的证明义务,并对其规格说明进行了一次精化.     

基于Web的网络旅游服务系统的形式化B开发

形式化B方法支持从规格说明到代码生成的全部软件开发过程。结合网络旅游服务系统模型，讨论了形式化B方法的具体运用，在分析服务器端和客户端状态表示的基础上，给出了该系统的抽象机模型及其精化过程。     

面向方面分布式系统形式化规格说明语言

分布式系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要面向方面软件工程方法的支持,而形式化方法能保证分布式系统的正确性。本文对分布式规格说明语言Ocsid进行了面向方面的扩展,讨论了面向方面的Ocsid的框架结构、语法要求、方面的联结和功能接口。定义了面向方面的Ocsid规格说明语言中叠加和组合的形式化描述,该形式化描述覆盖了各个精化阶段,使精化体系的各个独立视点被协调地组合,并能形式化地验证规格说明的时态属性和系统行为。本文的工作针对的是分布式系统的形式化规格说明,提出了面向方面Ocsid的形式基础和方面扩展,其基本思想同样适用于更一般的情况。     

一种状态图到B规格说明的自动转换方法研究实现

状态图是UML动态视图之一,主要描述对象的动态行为,但缺乏形式化的动态语义,不利于软件从需求到代码的自动化转换。B语言支持形式化规格说明,在MDA转换过程中,把UML状态图转换为B规格说明,可以使MDA中的需求表达得更为精确。基于此,提出了一种基于EMF的状态图到B规格说明的转换方法,设计了状态图和B抽象机的元模型,定义了元模型之间的转换规则,给出了该规则的ATL描述,最后在Eclipse平台实现了状态图到B规格说明的自动转化。该方法为MDA过程中获取形式化需求提供了一种新的途径。     

两次数据精化的形式化软件开发方法

提出了一种从数据精化、过程精化、再数据精化的两次数据精化的形式化软件开发方法。传统Z规约数据精化很复杂。该文先采用过程写出初始规范,对模式进行第一次数据精化,然后把它转换为Z模式,再进行过程精化。最后再数据精化到且标代码。以常见动态Web网页脚本语言PHP为例,阐述了该方法。并为此写了一套从过程到Z模式的转化规则,以及精化到PHP的精化规则。     

基于Event-B 方法的多应用智能卡的建模与开发

Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型。提出了如何将Event B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面重写需求,明确精化策略;然后利用形式化方法建立抽象模型并验证该模型;最后,在正确的抽象模型上按照精化策略添加需求、逐层精化,并对每层模型进行验证,基于满足需求的最后一层模型,可进一步利用工具完成代码自动生成。该方法学采用精化理论,以逐层递增的方式明确被开发系统的需求及性质,并进行形式化建模与验证,确保了模型的正确性。为了说明该方法学的可行性,以真正工业界的多应用智能卡为实例,基于Event-B方法及其工具平台Rodin给出了该方法在实际建模及验证过程中的应用。     

用Petri网描述程序精化中的循环不变式

形式化方法把程序看成规范,形式化开发方法包括形式规范和规范(程序)的精化.精化演算方法能够通过演算的方式,把规范逐步精化为程序.然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的.形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序.因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索.     

一种基于模型的创建形式化规格说明的方法

本文介绍一种基于模型的从非形式化规格说明文档中提取形式化规格说明的方法。本方法对非形式化的规格说明采用了结构化分类和渐进的当非形式化的规格说明可以被归结成能用某一种规模说明语言表示之后，渐进优化就结束了，对于如何将需求的变化、已有的自动化支持以及非形式化的设计集合到优化技术中，给予了指导。本方法在设计ＲＳ２３２中继器的应用中已得到了检验。     

用Petri网描述程序精化中的循环不变式

形式化方法把程序看成规范,形式化开发方法包括形式规范和规范（程序）的精化。精化演算方法能够通过演算的方式,把规范逐步精化为程序。然而,演化的过程依赖于开发人员的经验,整个过程全部都是手动的。形式化方法的最高目标是软件自动化,使得能从规范自动开发出正确的程序。因而用Petri网来描述程序精化中的循环不变式,希望以此作为软件自动化的一个探索。     

基于UML和Z的软件体系结构求精方法及其应用

论文探讨了如何将可视化建模语言UML和形式化描述语言Z集成而得到一种新的求精方法,寻求一种在软件体系结构求精过程中UML到Z的映射与转换机制。最后通过使用这个新的求精方法对一个实例求精来描述整个求精过程。     

精化演算支撑工具的分析

利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具RT(RefinementTool),对精化工具进行了需求分析和功能分析。在精化工具的设计中,分析了精化工具的设计目标、总体结构、精化与证明的表示方法、用户界面和工具的扩充性等问题,通过对精化和证明的表示方法的分析,提出了一种精化与证明的表示相结合的方法。     

一个基于Web技术的网络银行系统的B方法设计与实现

B方法作为少数几种具有较强商业化工具支持的形式化方法之一,支持规格说明到代码生成的全部开发周期。文章将B方法应用于网络银行系统模型开发。此方法提供了系统的需求和可执行代码之间的中间过程。整个开发过程中的规格说明书写以及细化都使用Atelier B。     

OOZE求精技术自动化的探讨

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

基于C++模板的Z规格说明的数据类型的实现

主要介绍了用C++类模板实现Z规格说明语言中的类型,包括数据结构的设计、成员函数的设计。该模板的实现便于代码的重用和简化求精,从而提高软件开发的效率。     

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

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

Radl 形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.