UML顺序图的自动验证

UML顺序图反映了系统中并发对象之间的消息交互及顺序,在软件建模中占有重要地位。该文对UML顺序图模型的自动验证方法进行了研究,在把UML顺序图转换为Promela语言后,使用模型检验器SPIN来验证系统设计模型是否满足某些关键性质需求。为了加强该方法的适用性,采用可扩展的标记语言XML文件格式定义顺序图模型的外部表示形式,该表示方法遵从OMG的XMI标准,从而使验证过程适用于不同的UML建模环境。     

Integrating Model Information in UML Sequence Diagrams

In a UML model, different aspects of a system are covered by different types of diagrams. Nevertheless, it is important to provide means to check the consistency and completeness of the UML model. This problem is addressed in this paper by integrating the information specified in class and statechart diagrams into sequence diagrams. The representation as constraints attached to certain locations of the objects lifelines in the sequence diagram allows the identification of gaps and contradictory specifications. Furthermore, dependencies between the sequence diagrams can be investigated based on the previous analysis.     

UML时间顺序图的可达性分析

对于实时系统来说,UML顺序图描述了对象之间的交互。对象之间的交互展现了系统行为的场景。本文中,我们针对描述多场景的UML顺序图组合中的可达性问题进行研究。尽管这个问题可以转换为相应的时间自动机,然后进行处理,但其转化为之后,状态空间巨大,解决的开销比较大,效率不高。针对部分可达性问题,本文采用更为高效的基于线性规划的解决方案,其思想如下:首先遍历所有到达给定节点的简单路径片断来验证可达性,随后遍历到达给定节点的并且包含所有循环至多一次的路径片断来验证可达性。由于我们并没有遍历所有路径片断,因此用本文的方法判定给定节点的可达性的时候,结果会有三种:可达,不可达和不确定。由于有些循环与可达性是无关的,我们进一步通过识别哪些循环与可达性无关,对算法进行改进。     

基于UML顺序图测试用例的生成

在分析UML模型可测试性的基础上,提出一种基于UML顺序图模型生成分布式系统测试用例方法,以系统软件配置项为对象对分布式应用典型场景进行模拟,通过解析MDL文件给出对顺序图XML的建模方案,实现一个自动生成分布式系统测试用例工具。实验结果表明,生成的测试用例达到判定覆盖的标准,具有良好的应用前景。     

Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification

UML 2.X sequence diagrams(SD)are among privileged scenarios-based approaches dealing with the complexity of modeling the behaviors of some current systems.However,there are several issues related to the standard semantics of UML 2.X SD proposed by the Object Management Group(OMG).They mainly concern ambiguities of the interpretation of SDs,and the computation of causal relations between events which is not specifically laid out.Moreover,SD is a semi-formal language,and it does not support the verification of the modeled system.This justifies the considerable number of research studies intending to define formal semantics of UML SDs.We proposed in our previous work semantics covering the most popular combined fragments(CF)of control-flow ALT,OPT,LOOP and SEQ,allowing to model alternative,optional,iterative and sequential behaviors respectively.The proposed semantics is based on partial order theory relations that permit the computation of the precedence relations between the events of an SD with nested CFs.We also addressed the issue of the evaluation of the interaction constraint(guard)for guarded CFs,and the related synchronization issue.In this paper,we first extend our semantics,proposed in our previous work;indeed,we propose new rules for the computation of causal relations for SD with PAR and STRICT CFs(dedicated to modeling concurrent and strict behaviors respectively)as well as their nesting.Then,we propose a transformational semantics in Event-B.Our modeling approach emphasizes computation of causal relations,guard handling and transformational semantics into Event-B.The transformation of UML 2.X SD into the formal method Event-B allows us to perform several kinds of verification including simulation,trace acceptance,verification of properties,and verification of refinement relation between SDs.     

基于MDA的UML模型转换技术——从顺序图到状态图

为了实现不同中间件平台之间的集成和互操作,OMG提出了一个标准的基于模型的体系结构:MDA。MDA将应用模型划分成与平台无关的模型(PIM)和与平台有关的模型(PSM),并定义了PIM和PSM之间的4种映射关系。该文主要对PIM到PIM之间的映射进行了研究。该映射实质上是PIM模型的精化,其主要方面是分析模型和设计模型之间的转换。MDA使用UML来描述各种模型。UML是一种可视化的通用的面向对象的建模语言。UML顺序图主要用于需求分析,而状态图在系统设计阶段起重要作用。该文介绍了一种从UML顺序图中合成状态图的方法,合成的过程基本上是自动完成的,只需要很少的用户交互,从而为PIM模型的精化提供有力的支持。     

基于UML顺序图的安全苛求软件安全性分析

安全性分析对于确保开发出符合安全性需求的软件系统非常重要。该文从安全苛求软件的建模特点出发,分析现有的安全性分析方法和UML建模语言在安全苛求软件方面的应用及优缺点。针对UML面向安全性需求建模的不足,对顺序图增加了安全性描述方法。通过车载ATP系统的建模应用验证其可行性与有效性。     

UML2．0顺序图的XYZ／E时序逻辑语义研究

UML2．0顺序图适合于描述软件体系结构的各个组件之间和复合组件内部各个子组件之间的动态交互行为，但由于UML2．0顺序图的语义不够精确，使得它的描述结果不利于进一步的分析和验证。基于此，本文在定义UML2．0顺序图的语法和语法约束的基础上，给出了UML2．0顺序图的XYZ／E时序逻辑语义，为使用UML2．0顺序图与XYZ／E相结合的方式来描述软件体系结构的动态交互行为奠定了基础。     

带时间约束的UML序列图的分析工具

统一建模语言(UML)是一种多用途的可视化建模语言,它可用于软件系统的规约、可视化的构造和建档.UML序列图描述了交互对象间的协作,如在实时和分布式系统中通讯实体间的信息交互.与其它的规约和设计过程类似,UML序列图的规约也易出错,所以对它进行分析是很有必要的.文章描述了一个对带时间约束的UML序列图进行分析的工具.     

基于UML时序图的集成测试序列自动生成

该文研究了基于UML时序图的集成测试序列自动生成方法。该方法分析了时序图的语义信息并添加语义约束规约生成可测试模型,从中提取相关信息生成有限状态机;然后使用Wp方法构造测试序列;最后使用中国邮递员算法对Wp方法进行改进生成最优测试序列。该方法生成的测试序列长度相对较短,并能充分满足测试用例覆盖需求。     

基于UML顺序图的测试方法

本文描述一个在UML顺序图上生成测试用例的方法。我们使用带OCL约束的顺序图．即从类图和状态图中提取信息以OCL形式附加在顺序图的对象生命线的适当位置。首先检查顺序图的完备性和一致性。然后从顺序图中生成测试规格说明以及顺序图的事件系列。最后根据测试准则采用类似于类别一划分方法进行测试用例的生成。另外,我们将此方法应用于一个简化的DHCP协议．解释了方法的一般过程以及方法的可行性。     

The many meanings of open source

Many software development methodologies are called "open source." However simply stating that a project is open source doesn't precisely describe the approach used to support the project. A multidisciplinary viewpoint can help determine those characteristics that are common to open source projects and those that vary among projects. These characteristics form the basis for a taxonomy of open source projects that's useful for analyzing and setting up projects. They also provide a starting point for understanding what "open source" means.     

Toward the Reverse Engineering of UML Sequence Diagrams for Distributed Java Software

This paper proposes a methodology and instrumentation infrastructure toward the reverse engineering of UML (Unified Modeling Language) sequence diagrams from dynamic analysis. One motivation is, of course, to help people understand the behavior of systems with no (complete) documentation. However, such reverse-engineered dynamic models can also be used for quality assurance purposes. They can, for example, be compared with design sequence diagrams and the conformance of the implementation to the design can thus be verified. Furthermore, discrepancies can also suggest failures in meeting the specifications. Due to size constraints, this paper focuses on the distribution aspects of the methodology we propose. We formally define our approach using metamodels and consistency rules. The instrumentation is based on aspect-oriented programming in order to alleviate the effort overhead usually associated with source code instrumentation. A case study is discussed to demonstrate the applicability of the approach on a concrete example     

动静态信息相结合的UML2．0序列图逆向生成方法

符合UML2.0标准的序列图在UMLl.x序列图的基础上添加了控制流信息.为此,本文提出一种基于动静态信息相结合的UML2.0序列图逆向生成方法.该方法首先利用目标程序运行时的动态信息产生基本的方法调用序列,然后依据静态的程序依赖图对其进行补充和调整,在其上添加方法间的逻辑关系,使产生的序列图带有控制流信息.这种方法生成的序列图符合UML2.0标准,可以很好地辅助用户理解目标程序.     

基于UML2.0序列图的Web服务运行时验证方法

陆空通话标准用语(英语)的训练是空管模拟训练中的重要内容。对空管模拟训练中的语音指令自动识别问题进行了分析研究,包括:陆空通话标准用语基本特征的分析、语言模型的文法描述、指令特殊发音的识别处理、识别后处理方法以及声学模型训练方法等,并基于Sphinx-4语音识别引擎,设计实现了一个语音指令识别系统AIRS(ATC Instruction Recognizer System)。系统实验数据分析表明,声学模型训练后的语音识别正确率可以达到空管模拟训练的需求。     

一个基于UML顺序图的场景测试用例生成方法

UML顺序图是基于UML开发的软件设计模型的重要组成部分,它描述了软件系统的动态行为,是软件集成测试过程中的一个重要的信息来源。本文提出了一个基于UML顺序图的场景测试方法,它以UML顺序图为主要测试模型,结合UML状态图和类图生成所有的测试场景,最后使用范畴一划分方法找到与每一场景相关的环境条件并将它与方法序列、输入、输出合理组合作为覆盖该场景的测试用例,用于测试该场景中对象之间的交互。由于UML已广泛用于软件分析和设计阶段,通过UML模型生成测试用例可充分利用已有的设计结果,减少测试阶段所需的费用,对于已使用UML的工业界有着重要的意义。     

基于事件确定有限自动机的UML2.0 序列图描述与验证

为了确保软件分析与设计阶段UML2.0序列图模型的可靠性,采用命题投影时序逻辑(propositional projection temporal logic,简称PPTL)模型检测方法对该模型进行分析和验证.提出了事件确定有限自动机(event deterministic finite automata,简称ETDFA),并使用该自动机为序列图建立形式化模型,通过给出的基于ETDFA的PPTL模型检测算法得到验证结果.该方法可以在基于Spin的PPTL模型检测器的支持下实现.实例结果表明,该方法可以验证序列图的性质并保证其可靠性.     

UML活动图的正确性检测

UML(统一建模语言)活动图广泛用于软件开发过程,然而它是半形式化的模型,不能进行推理,无法保证其正确性。为了保证它的正确性,必须先把它转化为形式化模型再进行检测。现有工作已将活动图转换成变迁系统、进程代数、Petri网等模型,需要增加或丢失大量信息。本文提出一种新的方法,该方法直接将活动图转换成被称为依赖结构的形式化模型,不会增加或减少活动图的任何信息。基于依赖结构模型我们首先讨论了检测活动图的正确性方法,然后介绍相应的工具;最后用一个实例来详细说明检测过程。该工作有助于软件工程师正确地使用UML活动图对软件系统进行分析和设计。