State Based Static and Dynamic Formal Analysis of UML State Diagrams

Design and specification is a serious issue in software engineering because of the semantics involved in transforming the real world problems to computer software systems. Unified Modeling Language (UML) has been accepted as a de facto standard for design and specification of object oriented systems. Unfortunately, UML structures lack defining semantics of a system. Formal methods are proved powerful, particularly, at requirement specification and design level. For a moment, formal methods are not welcomed because of much use of mathematics in formal languages. Therefore, a linkage between UML and formal methods is required to overcome the above deficiencies. In this paper, a new approach is developed by integrating UML and Z specification focusing on state diagram considering both the syntax and semantics. It is believed that this new approach will be effective and useful both at academics and industrial level. The resultant formal models of the approach are analyzed and validated using Z/Eves tool.

基于WF StateMachine的UML状态图动态构建与测试

采用UML分析与设计的业务信息系统,业务流程经过层层的抽象迭代,缺乏一种透明的业务流程实现。WF提供了可视化的业务过程编程模型,便于实现业务流程自动化,在对比分析WF State Machine和UML状态图的基础上,研究从UML状态图到WF State Machine业务流程映射关系,选取UML中典型状态图,依据一定的命名转换规则,实现了从UML状态图分析设计到WF状态机业务过程可视化的构建,完成了动态测试。

基于WF State Machine的UML Communication Diagram动态构建及测试

在基于UML的业务流程分析与设计过程中,从静态模型分析到动态模型构建,经过一系列抽象转换和代码实现,往往满足不了业务需求,缺少一种所见即所得的业务过程实现。在探索UMLCommunicationDiagram和WF StateMachine业务流程映射关系的基础上,选取UML用户指南中典型案例,研究从CommunicationDiagram到State Machine编程模型之间的静态映射和动态规则转换,基于WF可视化地实现了动态构建与测试,解决了从分析、设计到构建的无缝转换。

带有并发行为的UML状态机图的形式语义

在软件开发过程中,UML(统一建模语言)状态机图是目前最流行的建模形式之一,它属于半形式化模型,无法用形式化的方法进行推理。为了能对UML状态机图进行推理,现有工作采用Petri网、时序逻辑语言XYZ/E、动态描述逻辑、Z(Object-Z)语言、CHAM化学抽象机等作为状态机图的形式语义,但这些语义都是行为语义,并没有从结构上直接形成体现真并发的形式语义。该文提出一种新的模型——统一结构模型作为带有并发行为的UML状态机图的形式语义,该模型不会增加或减少状态机图的任何信息。基于统一结构模型首先定义了状态机图的格局(全局状态),用于表现状态机图的执行过程,并且给出了UML状态机图的格局的转换规则,说明格局如何在状态机图中执行,在此基础上给出了状态机图的可达性算法,然后还对状态机图的死锁等性质进行了介绍,最后开发出一个原型工具,实现了状态机图的可达性分析,并用实例说明了该方法的应用。

基于UML状态图的PLC程序测试路径生成方法

为了提高可编程序控制器程序的测试效率,提出一种基于统一建模语言状态图的可编程序控制器程序测试路径生成方法。这一方法利用反蚁群算法生成测试路径,可以避免测试路径过多导致的爆炸问题。通过人工蚂蚁搜索未被遍历或信息素最小的顶点,得到测试路径,在满足测试路径充分性覆盖准则的同时,确保数量适中。通过案例试验,验证了方法的可行性和有效性,能够避免与其它文本重复。

UML模型在信息系统需求分析中的应用

系统需求分析是软件信息系统开发活动的起始环节,使用UML模型进行软件需求分析是目前面向对象的需求分析方法的一种重要方法,根据不同软件系统的需求描述,选取适当的UML分析模型从不同的角度对需求中的功能点进行描述,可以使系统用户、需求分析人员以及未来的设计开发人员能通过多个角度观察目标系统的应用场景、业务流程、系统对象的状态变化;从抽象的维度了解目标系统的功能、系统对象之间的关系、业务规则和约束。通过一个用于车辆管理的信息化系统的需求分析过程,分别探讨了用例图、活动图(业务流程图)、状态转换图三种UML模型的适用场景和使用方法,以及在实践工作中的注意事项。为相似的信息化系统的需求分析实践提供一种可供参考的操作方法。

基于UML状态图的类测试用例自动生成方法

UML作为面向对象软件开发的事实上的标准建模语言，近年来得到了广泛的应用 ，基于UML的测试也成为面向对象软件测试的研究热点。该文把基于扩展的有限状态机EFSM 的唯一输入输出UIO测试用例自动生成方法和UML的类的状态图相结合，提出了一种基于UML 状态图的类的测试用例自动生成方法。

UML状态机的形式语义

许多大型系统在进行分析和设计时,均采用UML作为需求描述语言,尤其是一些对安全性要求较高的系统,更是广泛采用UML的动态行为描述机制——状态机来描述协议及控制机制.但是,由于UML没有形式化的动态语义,不利于对其所描述的需求进行形式化验证和证明,为了解决这一问题,采用以下方法为UML状态机构建形式语义.把UML状态机中的状态映射到一种项代数上,用归纳的状态项表示状态机的状态.然后,把状态项映射到一种加标记的变迁系统LTS上,LTS-状态是状态机的状态项,LTS-变迁是UML状态机的微步.最后,用Plotkin风格的结构操作语义SOS(structural operational semantics)规则归纳地给出满足组合性的UML状态机语义.此方法既是对一些经典Statechart形式化方法的综合,又针对UML状态机的特点作了创新,使状态项能够动态地描述任意时刻UML状态机的配置树,简化LTS的标记,同时,结构化的语义规则更为形式化验证奠定了基础.

基于UML状态机与B方法的高可信嵌入式软件开发

提出了一套集成UML与B方法开发高可信嵌入式软件的实用方案:以软件的UML状态机模型为起点,将其转换为B抽象模型并在B工具中验证该模型的一致性,然后遵循B模型逐步精化的开发规则,利用B方法的精化正确性验证功能,得到系统的可靠的实现模型,最后借助B工具自动生成C代码。实例分析表明,这套方法可以提高高可信嵌入式软件的开发验证效率。给出了嵌入式软件设计中常用的UML并发状态图到B抽象模型的转换规则。

基于UML的面向对象软件测试系统

设计和实现了一个基于UML的C++测试集成开发环境CppTestIDE。它以基于UML的分析设计规约文档作为OO软件测试的重要依据,通过对UML文档的词法语法分析,提取类状态机信息;采用手工和自动生成测试用例;并根据生成的测试用例构造驱动模块,生成测试装置。同时,对源代码插装,以便度量代码覆盖率。在此基础上,编译测试装置和源代码,生成测试装置执行文件。最后,驱动测试装置执行文件,分析测试结果,生成测试报告。

UML状态机到B形式化规约的转换

文章研究在高可信软件工程中集成形式化方法。以软件设计的UML状态机模型为起点,将其转换为B形式化模型,然后在B工具环境中遵循B方法的精化原则和正确性验证方法,开发出可靠的实现模型。提出一套从UML状态机到B形式化规约的转换规则,涵盖UML基本状态图、分层状态图和并发状态图。实例分析表明,这套转换规则行之有效。

UML状态机的模型检验方法

模型检验是一种确保设计规范正确性的形式化自动验证技术 ,本文提出了对 UML状态机进行模型检验的方法。文中首先对 UML状态机的语法和语义进行描述 ,然后基于语义中的 RTC步给出生成状态机全局可达状态迁移图的方法 ,方法的核心是在当前格局下根据使能条件确定所有的最大无冲突迁移集。文章最后给出算法以验证 UML状态机是否满足用计算树逻辑 ( CTL)

基于UML状态图测试的充分性准则

本文描述了基于UML状态图生成测试用例的充分性准则。在测试时,循环被执行一次是很不充分的,本文提出了使循环分别执行0次、1次、2次,即ZOT循环覆盖准则,在此基础上本文还提出了全ZOT路径覆盖准则,并给出了这些覆盖准则的应用,讨论了这些覆盖准则之间的包含关系。

基于改进蚁群算法UML状态机图的测试用例生成

为了减少测试工作量,防止测试用例数目过多而导致爆炸,提出了使用改进的蚁群算法直接从UML状态机图中生成测试用例的方法。利用UML状态图是对系统可能的生命历程进行建模,由于状态图具有直观性,所以简化了生成测试用例过程,从而减少了测试的工作量。通过构造人工蚁群以及动态更新信息素矩阵,让蚂蚁选择还没有搜索或边信息素最小的顶点,确保了测试用例的数量既满足测试需求,又不会过多。通过编写算法及模拟仿真,对该算法的可行性和有效性做了验证和仿真分析。

基于UML实时状态图的定量分析

在实时系统的开发过程中,时间上的约束在系统早期的定量分析中起着非常重要的作用。UML作为一种图形化、面向对象的建模语言,其中的实时特性描述文件UML Profile for Schedulability,Performance and Time适用于对实时系统的刻画。在给定系统的实时状态图基础上,用相对应的随机Petri网模型进行定量分析,得到实时系统最终的分析结果,对系统开发有重要的指导意义。

基于UML状态图的类状态测试

在介绍UML状态图的基础上,以面向对象软件的类作为基本测试单元,研究了基于UML状态图的类状态测试技术,并在Eclipse平台上结合Java工具用手工选择测试数据进行了实例测试。

UML状态图到形式化B语言转换的实例研究

使用UML中的状态图可以帮助描绘生物领域中碰到的很多问题,而形式化B方法能为生物系统建模并提供严格的证明,UML和B的结合可产生一种形式化的UML,并精确地用B方法建模。对免疫因子网络中T细胞免疫状态的UML状态图进行了两种方法的形式化,并进行了比较。

基于UML状态图的C4ISR系统的建模和实时分析

针对C4ISR系统的实时性强的特点,对UML状态图进行时间扩展,使用时间扩展的UML状态图对C4ISR系统进行建模。同时为分析C4ISR系统的实时性,采用一定的转化规则,将时间扩展状态图模型转化成时间Petri网模型,使用时间Petri网的可达树来分析C4ISR系统的时间特性。应用一个C4ISR防空实例表明了该方法的可行性和实用性。

应用UML开发智能继电保护的整定计算程序

电力系统复杂应用软件的开发必能采用先进的软件工程学方法。统一建模语言 ( U nified Modeling L anguage,U ML )是近年来软件工程领域内取得的最重要成果之一。文章介绍了 UML 的产生背景及特点 ,然后详细讨论了 U ML在智能继电保护整定计算及管理系统 ( ICAPE)开发中的应用。结果表明 ,统一建模语言 ( UML )具有标准性、系统性、可视化、自动化等优点 ,在电力系统复杂软件的开发中 ,将其合理地应用于软件开发的各个阶段 ,有助于提高软件开发效率及软件质量。因此 ,UML

基于UML状态图的类测试用例实现的研究和设计

UML状态图能有效的表现系统的并发控制和类的嵌套,但用其实现的类测试用例复杂。研究了UML状态图和扩展有限状态机这两种方法在软件测试中状态转换的特点,利用扩展有限状态机状态转挟单一线索化的特点降低UML状态图在类测试用例生成中的复杂性。以一个坐标图形显示类的测试用例生成为例,详细讨论了结合扩展有限状态机状态转换特点的UML状态图在面向对象测试技术中的应用。