UML活动图的形式语义及分析

UML活动图缺乏精确的动态语义,不利于对其所描述的系统进行形式化的分析、验证和确认。为此,论文结合Petri网给出了包含对象流状态描述的UML活动图的形式语义,并据此对UML活动图的典型流程和其所描述的动态系统的正确性进行了分析。该形式语义覆盖了UML活动图的绝大部分特征,为精确描述工作流程并对其进行分析奠定了基础。     

UML活动图的操作语义

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

An object-oriented approach to formally analyze the UML 2.0 activity partitions

Nowadays, UML is the de-facto standard for object-oriented analysis and design. Unfortunately, the deficiency of its dynamic semantics limits the possibility of early specification analysis. UML 2.0 comes to precise and complete this semantics but it remains informal and still lacks tools for automatic validation. The main purpose of this study is to automate the formal validation, according a value-oriented approach, of the behavior of systems expressed in UML. The marriage of Petri nets with temporal logics seems a suitable formalism for translating and then validating UML state-based models. The contributions of the paper are threefold. We first, consider how UML 2.0 activity partitions can be transformed into Object Petri Nets to formalize the object dynamics, in an object-oriented context. Second, we develop an approach based on the object and sequence diagram information to initialize the derived Petri nets in terms of objects and events. Finally, to thoroughly verify if the UML model meets the system required properties, we suggest to use the OCL invariants exploiting their association end constructs. The verification is performed on a predicate/transition net explored by model checking. A case study is given to illustrate this methodology throughout the paper.     

一种UML活动图的逆向恢复方法

UML活动图的逆向恢复是逆向工程的重要组成部分,对于理解目标系统的动态行为和控制流程有重要辅助作用。论文针对Windows环境中的面向对象系统,给出了一种基于进程(线程)间关系的UML活动图的逆向恢复方法,该方法采用反射植入机制对目标系统进行基于关键函数的植入,然后对植入后目标系统运行时的动态信息进行过滤并提取出来转化为UML活动图模型文件。在此过程中给出了相应的植入和过滤算法,并通过实验验证该方法的有效性。     

基于UML活动图化简方法的工作流模型校核研究

针对开放、响应型系统建模UML活动图表现优良的特性,UML活动图在工作流建模领域也引起了人们的极大关注。然而相关的研究仅仅起步,特别是针对相应的模型校核技术更是研究甚少。该文提出了基于UML活动图化简方法的工作流模型校核技术,在UML活动图到活动超图映射基础之上,对活动超图建立化简规则,通过化简实现工作流模型校核。实践证明此方法有效。     

UML行为图驱动的Java程序运行时验证工具

UML是一种标准的可视化建模工具，广泛应用于软件系统的描述、可视化、构建和建立文档。本文介绍了一种UMI。行为图驱动的Java程序运行时验证工具。该工具以一个随机的测试用例集作为输入，运行经过插装的被测Java程序，得到一组用于验证的程序运行轨迹。通过对程序运行轨迹和UML行为图中合法的事件序列的比较，该工具可以对程序的动态行为规约进行检查。本文描述了该工具的设计思想、算法和实现技术，并通过对实例研究对该工具的可用性和有效性进行了讨论。     

工作流异常处理的UML活动图描述方法

提出了用UML活动图描述工作流异常处理的方法.根据工作流系统特点,对UML活动图作适当扩展,为扩展后的活动图定义了的形式化语句,通过实现一个RCT步来描述一个潜在发生的异常状况,并对不同处理策略下的处理过程进行了描述.结果使得UML活动图适合描述含有异常的工作流系统;由于是采用了UML建模语言,编码实现更容易.     

UML建模技术在医院奖金核算系统中的应用

针对当前医院信息管理系统没有科室奖金核算的缺点,结合医院奖金核算复杂性和特殊性的特点,提出应用UML建模技术设计开发的系统解决方案．本文分析面向对象的UML建模技术,从系统开发过程的视角着重介绍了UML建模技术在需求分析和结构设计层次中的应用,提出了医院奖金核算管理系统开发问题的新思路．根据建模的用例图、活动图和序列图描述出系统设计的构架,用类图反映出数据对象的属性和操作．最终实现一个功能完善,性能可靠的医院奖金核算管理系统．     

Validation of static properties in unified modeling language models for cyber physical systems

Cyber physical systems (CPSs) can be found nowadays in various fields of activity. The increased interest for these systems as evidenced by the large number of applications led to complex research regarding the most suitable methods for design and development. A promising solution for specification, visualization, and documentation of CPSs uses the Object Management Group (OMG) unified modeling language (UML). UML models allow an intuitive approach for embedded systems design, helping end-users to specify the requirements. However, the UML models are represented in an informal language. Therefore, it is difficult to verify the correctness and completeness of a system design. The object constraint language (OCL) was defined to add constraints to UML, but it is deficient in strict notations of mathematics and logic that permits rigorous analysis and reasoning about the specifications. In this paper, we investigated how CPS applications modeled using UML deployment diagrams could be formally expressed and verified. We used Z language constructs and prototype verification system (PVS) as formal verification tools. Considering some relevant case studies presented in the literature, we investigated the opportunity of using this approach for validation of static properties in CPS UML models.     

基于进程代数的UML序列图的形式语义

UML序列图用于建模实例间动态交互过程．但UML规范并没有给出其形式化的动态语义，这不利于对模型进行形式化验证和证明。本文把序列图中的事件动作及其执行序列映射为进程代数中的进程表达式，利用进程代数语义框架来构建UML序列图的形式语义。首先，建立了序列图到进程代数的语义映射规则；然后用Plotkin风格的结构化操作语义给出并证明务件组合算子演绎规则；最后，归纳定义了算子次序约束条件并证明了其可终止性。     

基于UML和Petri网的锅炉仿真系统的研究

结合了UML状态图的表达特性和Petri网的分析特性,总结出状态图的设计步骤和状态图转化为Petri网的规则,并以国家质检总局科技项目-锅炉仿真系统为背景,对锅炉自动燃烧过程实例进行分析,按照设计步骤和转化规则,最终用Petri网描述出实例,为进一步分析系统特性奠定基础.     

一种基于场景的性质验证方法

顺序图是UML中重要的语法机制,用于对系统的动态行为进行建模。但是,建模后模型是否满足某方面性质却很难检验。为此,我们提出了一种基于场景的性质验证方法。该方法首先把描述一个场景的顺序图以及相关的状态图综合成一个“命题标记路径集”,把待验证的性质表示为有穷线性时序逻辑公式,然后利用“逆向标注”算法对其进行验
证。转化及验证过程均可自动完成。     

Real-time scheduling of batch systems using Petri nets and linear logic

This paper presents an approach to model, design and verify scenarios of real-time systems used in the scheduling and global coordination of batch systems. The initial requirements of a system specified with sequence diagrams are translated into a single p-time Petri net model representing the global behavior of the system. For the Petri net fragments involved in conflicts, symbolic production and consumption dates assigned to tokens are calculated based on the sequent calculus of linear logic. These dates are then used for off-line conflict resolution within a token player algorithm used for scenario verification of real-time specifications and which can be seen as a simulation tool for UML interaction diagrams.     

Synthesis of test scenarios using UML activity diagrams

Often system developers follow Unified Modeling Language (UML) activity diagrams to depict all possible flows of controls commonly known as scenarios of use cases. Hence, an activity diagram is treated as a useful design artifact to identify all possible scenarios and then check faults in scenarios of a use case. However, identification of all possible scenarios and then testing with activity diagrams is a challenging task because several control flow constructs and their nested combinations make path identification difficult. In this paper, we address this problem and propose an approach to identify all scenarios from activity diagrams and use them to test use cases. The proposed approach is based on the classification of control constructs followed by a transformation approach which takes into account any combination of nested structures and transforms an activity diagram into a model called Intermediate Testable Model (ITM). We use ITM to generate test scenarios. With our approach it is possible to generate more scenarios than the existing work. Further, the proposed approach can be directly carried out using design models without any addition of testability information unlike the existing approaches.     

UML在某型导弹训练模拟系统中的应用研究

文章以某型导弹武器训练模拟系统为研究对象,从需求出发,利用统一建模语言对该系统进行了分析,应用用例图、活动图以及协作图等对系统进行描述,采用静态结构建模和动态行为建模完成了对系统的建模分析,结果表明,应用UML可以优化设计过程,提高系统研发的效率,并且易于理解。     

UML模型及其应用

文章扼要介绍了ＵＭＬ的发展历史以及它与过程的关系,并针对ＵＭＬ的特色及存在的一些争议,结合一个从ＪＡＶＡ软件测试系统详细探讨了用例图、类图、活动图、交互图和包图的基本概念、基本思想、鲜明特色以及某些具体的应用问题,然后简要介绍了状态图和配置图,最后总结了ＵＭＬ的优缺点及适用范围。关键词##4面向对象;;ＵＭＬ;;过程;;用例;;类图;;活动图;;交互图;;包图     

基于UML的环境空间决策支持系统的分析与设计

统一建模语言(UML)是一种面向对象，定义明确的可视化系统建模语言，在地理信息系统工程的分析和设计中已逐渐被采用。以福建省海岸带环境调控空间决策支持系统为例，简述了系统建设背景和基本功能需求，研究了统一建模语言(UML)在空间决策支持系统分析和设计中的应用。重点提出了以系统需求用例图、活动图，类图和序列图为核心的UML辅助空间数据建模的基本原理和方法，并结合具体示例给出了基本操作流程过程和软件文档制品，最后给出了系统实现结果的典型用户界面。     

UML活动图的时序逻辑语义

UML活动图可以表示不同抽象级的控制流,很适合用于对系统的行为建模．但是缺乏精确的语义使得难以对它所表示的系统行为进行分析．XYZ／E是一可执行线性时序逻辑语言,既可描述系统的动态行为又可表示程序性质,用它对活动图形式化后,就可在统一的逻辑框架下分析活动图的性质．定义了一个有向图结构用以表示UML活动图,再给出其XYZ／E语义,并用一个例子说明活动图到XYZ／E的语义转换,为进一步的分析提供形式化基础．     

嵌入式系统描述与验证环境的实现

首先，用统一建模语言(UML)中的状态图描述系统在整个活动周期中所处的不同的状态，活动图表示状态图中每个进程的功能，对象约束语言(OCL)描述系统中的约束条件；然后，用自行开发的软件UML2SC将UML描述的系统转换成SystemC代码，以完成系统的模拟验证；并介绍了该方法的一个应用实例。     

Verification of real‐time systems design

The main objective of this paper is to present an approach to accomplish verification in the early design phases of a system, which allows us to make the system verification easier, specifically for those systems with timing restrictions. For this purpose we use RT‐UML sequence diagrams in the design phase and we translate these diagrams into timed automata for performing the verification by using model checking techniques. Specifically, we use the Object Management Group's UML Profile for Schedulability, Performance, and Time and from the specifications written using this profile we obtain the corresponding timed automata. The ‘RT‐UML Profile’ is used in conjunction with a very well‐known tool to perform validation and verification of the timing needs, namely, the UPPAAL tool, which is used to simulate and analyze the behaviour of real‐time dynamic systems described by timed automata. Copyright © 2009 John Wiley & Sons, Ltd.