UML模型形式化B方法转换的实现

UML是软件开发的标准语言,已经广泛运用于各种领域的软件设计建模之中。但是UML的半形式化表达方式缺乏准确的语义,使其无法在软件设计过程中针对需求的一致性进行分析,因此需要使用一种形式化方法对UML模型进行描述。以高速列车控制系统为例,基于B方法对用例图模型与顺序图模型进行形式化转换,对两种模型中各组成部分从语义角度分别进行了描述,从而完整地刻画了UML模型所描述的系统需求。     

基于UML活动图的测试研究进展

UML活动图不再是状态图的特例,它作为一种独立的模型广泛用于软件的行为建模.基于UML活动图的测试受到业界的普遍欢迎.然而从UML活动图自动生成完整的测试场景\用例成为一个难点.本文对基于UML活动图的测试进行了比较分析,总结了几种从UML活动图生成测试场景\用例的方法及其使用的算法,即反蚂蚁Agent方法、灰盒方法、自适应细菌Agent方法和系统的形式化方法.对这些方法进行了分析与比较,指出一些不足之处.最后对UML活动图测试的发展趋势做了一些展望.     

以UML用例图为基础的系统需求分析

UML是目前面向对象程序设计中的一种标准建模技术，它被用作确定、可视化、构建和文档化一个软件系统的结构。本文主要探讨以UML用例图为中心及出发点，类图、交互图为实现手段，捕获高层次的系统功能需求的策略。     

基于时序描述逻辑的UML顺序图形式化研究

在统一建模语言（UML）规范中顺序图的语义是以自然语言的形式描述的,是一种半形式化的语言,不能对系统的交互行为进行形式化分析及论证.针对UML顺序图缺乏精确的形式化描述问题,根据顺序图的时序特征,提出了增加交互操作符的UML顺序图的六元组形式化方法.对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑.应用时序描述逻辑的时态算子得到时序描述逻辑语义形式的UML顺序图.用UML顺序图描述完整的C语言执行过程,将其形式化描述,实验结果表明,这种方法是可行的.     

基于UML建模思想的查课系统的规划

本文论述了应用UML建模思想分析和规划了智能查课系统的开发过程,确定系统需求和要实现的功能。用表示系统静态特征的UML类图、用例图和描述系统动态行为特征的时序图对其开发过程进行了不同层面的描述,以便读者理解。     

UML用例图的Z形式规范

统一建模语言UML已经成为面向对象建模语言的标准，用例图在面向对象的软件开发过程中起着重要的作用，但是它缺乏Z形式语言的精确性。为了对它的描述更加精确，本文使用Z语言给出UML中用例图的形式化描述，并将其应用在一个简单的图书馆管理系统中。     

基于UML的网上花店系统建模分析

网上花店是电子商务的一种具体形式,其具有传统商店无可比拟的优势,本文分析了网上花店的具体需求,采用用例驱动的思想,利用UML建模语言完成了整个网上花店的功能抽象,需求建模,并用类图描述了系统的整体架构。     

UML与SDL结合使用的研究

1 引言在介绍如何将SDL与UML结合在一起使用之前,让我们先来回顾一下UML和SDL各自的适应范围。它们性能上的差异在于它们在工程应用中的不同的阶段。UML的非形式化的自然特性使其成为一种性能优越的建模语言,它应用完全的面向对象的分析(OOA)方法。然而对于实施,UML却不能胜任,通常要用传统的程序设计语言如C /Java来完成,而SDL的形式化定义使得它取代传统的程序设计语言有了可能。OOA与SDL相结合己有相当长的时间了,先用OOA(主要是类图和用例/概要)进行需求分析和识别对象,然后用SDL/MSC来精确定义系统的架构和系统的需求与系统的行为。很自然,我们可以用UML来进行需求分析,用SDL进行系统设计。     

UML类图的形式规约与精化研究

UML由于其广泛的应用和直观的图形化符号,成为了模型驱动工程的重要组成部分。但UML本身缺乏精确的形式语义定义,缺少对其模型精化关系的形式化规范定义,对UML模型进行形式验证变得尤为困难。UML类图作为描述系统结构的静态模型,不具备完整的形式语义。从UML类图的机械语义中抽取出形式规约,将UML类图中的结构和形式规约转换成定理证明器Coq中的机械语义定义。此外,还提出了类图的结构精化操作,将模型间的精化关系在Coq中进行形式化定义,并且对精化操作的原子操作进行机械验证,保证其精化前后系统的结构和语义保持一致。将UML和形式化方法相结合,为可验证的软件设计精化框架提供了理论依据。     

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

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

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

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

基于规则的用例规约验证方法

用例模型描述了参与者对系统功能的需求,在整个系统的开发过程中有着重要作用;用例描述若存在问题,会对系统开发造成很大影响。提出了一种用例规约的规则验证方法,通过分析用例规约中的错误类别,在特定的用例规约描述方法上设计了帮助发现规约中不完整性、不一致性错误的验证规则,并通过规则的形式化来支持需求的自动化验证。     

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.     

基于顺序图的FADEC软件需求状态图模型验证

基于模型的系统工程MBSE方法论在全权限数字电子控制(FADEC)软件开发领域的应用越来越普遍,模型作为开发过程中传递信息的介质,其在软件开发过程中的重要性不言而喻.完善的需求模型可以降低FADEC软件研制过程中的风险,提高研制效率.以SysML顺序图为测试用例,对模型进行测试.通过测试用例与需求的追踪关系,保证了测试的有效性.测试用例生成过程中利用了ATG用例自动生成技术.测试结果表明了此方法的实用性,实现了对需求模型的充分测试.     

用带时钟变量的线性时态逻辑扩充Object-Z*

Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首先用时钟变量扩充线性时态逻辑,接着提出了一个方法——用带时钟变量的时态逻辑(LTLC)来扩充Object-Z。用LTLC扩充的Object-Z是一个模块化规格说明语言,是Object-Z语法和语义的最小扩充,其最大优点在于它能方便地描述和验证复杂的实时软件规格说明。     

基于用例的需求建模方法

传统的软件需求规约是采用功能分解的方式来描述系统功能,而采用用例的方法进行需求获取和建模,是以用户为中心的建模方法.用例模型是由用例图和用例规约所组成的.用例图用来规定系统的行为,用例规约是用文档的形式对每个用例进行描述的.通过对银行系统进行基于用例的需求分析和建模,可以了解用例模型的益处.     

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

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

Object—Z规格说明的SQL动画模拟

软件规格说明的确认在软件开发阶段占有举足轻重的地位。形式规格说明的动画模拟技术是一种规格说明的确认方法。本文研究了Obiect-Z规格说明的SQL动画模拟方法，设计了从Object-Z到SQL的转换规则，并提出了模块封装的思想，即用存储过程表示类、对象和模式等模块，用户通过调用执行存储过程确认规格说明是否满足其需求。     

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

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