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

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

基于UMLsec的软件安全需求建模方法研究

安全性是现代软件系统的重要组成部分,安全需求建模是确保软件安全性的基础.针对软件安全需求,提出了一种基于UML安全扩展(UMLsec)的软件安全需求建模方法.在软件需求规格说明的基础上,获取安全需求,对安全需求进行描述,并将安全需求描述集成到功能需求模型中,构建安全需求模型,并对模型进行了验证.科研信息系统实例表明了该方法的有效性.     

带OCL约束条件的类图到object—Z规格说明的转换

如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法，为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的分析和验证技术架起了一座桥梁。本文定义如何将带0CL约束条件的类图转换到Object-Z规格说明的方法。这样不仅可以通过支持Object-Z语言的工具采对UML语言描述的系统性质进行验证和确认，而且能够帮助规格说明人员方便地构造Object-Z规格说明。     

一种获得形式化功能需求的方法

用例图在面向对象的软件开发过程中起着重要的作用。它用于描述系统的功能需求 ,但是它缺乏如Object -Z形式规格说明语言的精确性。本文结合一个实例给出了一种如何使用UML捕获系统的功能需求 ,并将该功能需求形式化的方法。本文定义了从UML用例图到Object -Z的转换规则 ,实现了用例图的形式化、获得了形式化的功能需求。     

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

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

Web应用的UML协作图建模与形式化规格说明

针对Web应用的特点,从整体功能层面和交互行为层面用UML协作图构建了Web应用模型,以便精确、有效地描述参与协作对象间的结构关系和交互行为,保证在利用UML形式的规格说明推导测试用例时所需的语义信息.研究了运用Object-Z语言来形式化描述Web应用模型,提出了相应的转换规则.设计了形式化规格说明自动化生成的工具(UMLTOZ)中的主要相关类库.     

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

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

基于UML的软件形式化需求分析与验证

针对软件开发中传统的需求分析方法所存在的需求描述不完整、具有二义性和不一致性问题,提出一种形式化需求分析方法。介绍根据用户需求采用形式化方法获取软件需求说明书并设计软件的统一建模语言（UML）模型的过程,及对该UML模型进行形式化描述,采用形式化验证技术对形式化后的UML模型进行需求验证,以确保设计的UML模型的正确性。实验结果表明,形式化的需求分析方法克服了传统需求分析方法中存在的问题。     

UML模型到B抽象机的转换和实现

统一建模语言UML广泛用于面向对象技术的建模,B方法主要是用抽象机来描述软件系统的规格说明.文章针对软件开发中经常用到的UML模型,提出了基于B语言的UML形式化方法:通过将UML模型转化为B抽象机,实现了UML模型的形式化.实例分析表明,转换是可行的.     

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

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

基于场景分析的系统形式化模型生成方法

采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径。当前的形式化安全分析方法,面临着系统的形式化建模难的问题。以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法。该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型。该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法。     

UML建模机制研究及在系统需求分析中的应用

对UML语言的组成结构和需求分析的基本原则做了简要的介绍,从两者之间的关系出发,提出了分析中的3类模型图,并导出了利用统一建模语言UML获得系统功能需求的方法和建模流程;从理论出发,在一个综合网管系统的设计中,从所得到的方法及建模流程图,结合图例详细阐述了需求分析建模所经过的5个阶段,从建立的3类模型图中得到一个较为完整的系统需求分析结论。     

Incremental development of UML specifications using operation refinements

In an incremental specification development process, operations are used to model dynamic aspects and can be refined gradually. We propose four kinds of operation refinement in order to control modifications when developing and refactoring UML specifications. Each refinement is described with its properties and illustrated by an example, showing which verifications can be done, using the B formal method.     

UML活动图的操作语义

越来越多的系统采用UML（unified model language,统一建模语言）作为建模语言来进行系统分析和设计.UML活动图是UML语言中描述系统动态行为的一种方法,它广泛地运用于业务建模.由于UML活动图缺乏精确的动态语义,所以不利于对其所描述的系统进行形式化的分析、验证和确认.为解决这一问题,根据UML1.5语义文档,给出UML活动图的形式化操作语义.首先给出UML活动图的形式化的语法,然后详细地定义了活动图的格局和变迁,最后基于LTS给出了活动图的演绎规则.主要工作是：引入状态包的概念,使得描述更加清楚、完善;通过LTS定义活动图的操作语义,并详细阐述演绎规则,从而获得活动图的全局状态转移图,使定义的操作语义很容易地应用到形式化验证中.该语义覆盖了UML活动图的绝大部分特征,为对UML活动图进行模型检验奠定了基础.     

自动产生一个图书馆的快速原型

AutoPA1.0是一套基于形式化方法的应用程序.它是一个基于需求规范而自动生成软件快速原型的Java代码的软件, 有着坚实、可靠的理论基础.给出一个图书馆管理系统的例子, 阐述如何用UML建立需求模型,然后用AutoPA1.0生成该需求模型对应的软件快速原型的Java代码. 采用的需求模型主要包括一个用况模型和一个概念类模型, 分别用UML中的用况图和类图描述.生成的软件快速原型将包括用况图中每个用例的执行,用一个系统数据库来描述当前系统状态, 该系统数据库保存了当前系统中存在的所有对象以及对象之间的关系.     

一种扩展UML/UP的需求分析方法

UML是面向对象分析和设计的工业标准;UP(Unified Process,统一过程)是使用UML作为建模语言的软件工程过程.UML和UP结合在一起成为一种很强大的软件工程方法学.UML/UP作为方法学,在需求方面存在两大不足:需求表达能力不强;需求表达与后续的系统分析和设计有较大的鸿沟.分析了需求工程中用例和场景分析以及用例图示的高层设计方法.在此基础上,提出了在需求方面增强了UML/UP方法.     

基于UML活动图的用例识别

在面向对象的软件开发过程中,统一建模语言(unified modeling language, UML)的用例图用于捕获用户的需求.传统描述用例的方法一般是开发者根据自己的经验,从需求中人工获取用例.然而,如何自动生成准确的用例仍然是一个待解决的问题.本文提出了一种通过用UML活动图半自动生成用例的方法.首先通过引入形式化模型——统一结构来描述用例图与活动图,其次给出分解活动图的算法,然后根据分解活动图得到的依赖链生成对应的用例的事件流,从而得到用例模型,最后通过所开发的原型CASE工具进行案例的演示,验证了本文所提出的方法的可行性。     

基于UML的医院门诊管理信息系统

UML是一种重要的面向对象软件开发方法,本文简述用UML进行系统建模的方法和步骤。以医院门诊管理信息系统为例,讲述如何利用UML对其进行需求分析、系统设计、实现及测试的具体过程。     

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

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