DEVS的面向对象可视化建模

DEVS是对离散事件系统的一种形式化描述,该文在DEVS中引入面向对象的方法,并采用UML（Unified Modeling Language)对它进行可视化建模。文中提出了基于DEVS的面向对象的一种建模规则和基于UML的可视化建模思想和方法,该方法是对DEVS和UML的扩充和改进。     

使用时间化自动机形式化带有时间扩展的UML状态图

严格建模是嵌入式实时系统设计的核心技术，通过UMI。方法与形式化方法结合可以给严格建模提供很好的工具支持。时间化自动机(Timed Automata)是一种用于描述、验证实时系统的理论模型。文中提出了一种通过时间化自动机来形式化带有时间扩展的UML状态图的方法，这种方法为UMI。与形式化方法的结合构造了桥梁作用。带有时间扩展的UML状态图用于嵌入式系统动态模型的建模，从时间化自动机模型得到形式化规范将更容易。UML状态图的形式化分为两部分完成；层次状态图的平面化以及时间化自动机的构造。     

基于时序描述逻辑的UML状态图语义

将UML图形转换成形式化规范是一种精确UML语义、扩大形式化软件方法适用范围的有效途径。鉴于描述逻辑强的可判定推理能力,提出一种采用时序描述逻辑形式化UML状态图,对描述逻辑进行时序扩展,得到可以表示动态和时序语义的形式化规范——时序描述逻辑,给出一套UML状态图向时序描述逻辑表达式转换的规则,通过实例验证了该方法的可行性。     

UML-BD在C3I系统中的应用

DEVS是对离散事件系统的一种形式化描述,它提供了一种层次的模块化的系统说明方法。该文中的UML-BD（UML Based on DEVS）方法就是在UML中结合DEVS这一特点,对UML进行一定的扩展;同时还在UML中还增加了时间的约束．满足系统的实时性的要求。基于C3I系统的层次性、实时性的特点,该文采用UML-BD方法对系统进行建模,构建出系统模型能够充分地展现系统特点。     

离散事件系统规范DEVS研究

离散事件系统是一类常见的系统，如何对这类系统进行描述与建模是离散事件系统仿真研究的核心内容。离散事件系统规范DEVS是一种离散事件系统形式化描述方法，它具有层次化和模块化的特点，利用该方法可对复杂的离散事件系统进行建模、设计、分析和仿真。该文详细介绍了DEVS基本模型和耦合模型，给出了DEVS在耦合运算下的封闭性构造证明，并提出了一种具有嵌套层次结构的DEVS耦合模型实现算法，该算法对基于DEVS描述的离散事件系统的仿真实现具有一定参考价值。     

一种基于CSP的面向方面状态图形式化描述方法

面向方面通过分离关注点解决软件系统中的横切问题,通过扩展UML可实现对面向方面的建模。本文利用UML的扩展机制将方面加入状态图中,描述了状态图中的方面与核心组件以及方面之间的编织,然后利用进程代数的形式化语义描述了扩展后的UML状态图,克服了扩展UML描述状态图的缺乏形式化动态语义,不利于对模型进行形式化验证和证明的缺
点。最后,以ATM自动取款机为例验证了基于CSP的面向方面状态图形式化描述的有效性。     

基于rCOS的UML状态图语义研究

统一建模语言（UML）中的状态图用于描述类的对象所有可能的状态及事件发生时状态的转移条件,从而进行系统动态分析。针对现有关于UML状态图形式化语义研究中存在的不足,该文提出基于统一程序设计理论的对象精化演算系统,用于描述UML状态图的形式化语义,给出与类图、序列图的一致性检验,为模型驱动开发提供了可行性。     

UML状态图的形式化描述

面向对象模型的形式化是形式化研究的重点,UML是一种得到承认的标准建模语言,CHAM是一种广泛用于异步并行计算和系统体系结构建模的语言,它适合对系统的状态变化进行动态的描述.利用和改进原有的CHAM建模语言,使其能够对UML状态图进行形式化描述.     

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

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

一种基于描述逻辑的UML模型验证方法

针对UML模型中可能会存在的概念不一致、概念冗余等语义一致性问题,该文提出一种基于描述逻辑的UML模型形式化与模型验证方法。该方法首先采用描述逻辑的子系统SHOIN（D）形式化描述UML类图、状态图以及活动图的基本模型构造,进而将UML模型转换为相应的描述逻辑本体,最终借助现有的本体推理机制验证UML模型的语义一致性问题。该方法可以为下一代的软件CASE工具实现软件模型自动推理和验证提供一种可选的技术方案。     

Activity-based DEVS modeling

Use of model-driven approaches has been increasing to significantly benefit the process of building complex systems. Recently, an approach for specifying model behavior using UML activities has been devised to support the creation of DEVS models in a disciplined manner based on the model driven architecture and the UML concepts. In this paper, we further this work by grounding Activity-based DEVS modeling and developing a fully-fledged modeling engine to demonstrate applicability. We also detail the relevant aspects of the created metamodel in terms of modeling and simulation. A significant number of the artifacts of the UML 2.5 activities and actions, from the vantage point of DEVS behavioral modeling, is covered in details. Their semantics are discussed to the extent of time-accurate requirements for simulation. We characterize them in correspondence with the specification of the atomic model behavior. We demonstrate the approach with simple, yet expressive DEVS models.     

基于UML的CPN模型在软件测试中的应用

UML在被工业界广泛接受的同时也成为学术界遵循的一种标准建模语言。许多面向对象软件测试的研究都围绕UML模型开展。但UML模型属于半形式化模型,往往无法自动生成测试用例。将UML模型与Petri网相结合,能够弥补其数学支持的不足。文章给出了基于UML的CPN模型的测试框架和一个从UML模型构造CPN模型的算法,并根据该方法给出了自动化支持工具U2CPN的类图结构。     

基于对象着色Petri网的UML模型研究

UML广泛应用于软件建模,但缺乏有效的模型检测的方法,使用形式化方法对UML模型进行分析,可以发现UML模型的设计问题,提高UML模型的质量。对象着色Petri网是一种拥有接口库所的模块化着色Petri网,既是一种图形化建模工具,又是具有严格的语法语义定义的形式化方法。通过引入事件托肯,改进了将UML模型转换为对象着色Petri网的方法,结合实例将UML状态图和协作图映射为对象着色Petri网模型。并用着色Petri网的方法和工具对模型进行了分析,验证了模型的一系列性质。     

UML顺序图的自动验证

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

REALIZATION THEORY OF DISCRETE-EVENT SYSTEMS AND ITS APPLICATION TO THE UNIQUENESS AND UNIVERSALITY OF DEVS FORMALISM

Many man-made systems have discrete event nature. Many modeling formalisms for discrete-event mechanisms have invented and been used for many problems. Among those models, the DEVS formalism is to provide natural and universal models in some sense.

This paper first provides a realization theory of general discrete-event systems. That is, a behavioral definition of discrete-event system is defined, and then a state transition function of the system is constructed. Based on the realization, the uniqueness problem of representations for discrete-event systems is positively solved. Furthermore, as an application of that solution, this paper shows both the fact that a legitimate DEVS with surjective internal transition function is unique up to isomorphism in the class of state representations of the state system defined from the DEVS, and the fact that any discrete-event system has a DEVS realization. In this sense the DEVS modeling facility has the uniqueness and universality in modeling discrete event mechanisms.     

UML模型到FSM模型的转换

通常可采用UML的各种图从Web应用不同方面对其进行建模.当对Web应用模型进行测试和验证时,需要分别考虑这些采用了不同图形描述的模型,这就带来了测试和验证的繁琐.如果将UML各种图转换到有限状态机(FSM)模型,则可以统一用FSM模型来表示、验证和测试.提出了基于状态迁移特性保持规则的UML到FSM的模型转换方法,特别针对UML状态图中的3种基本组成单元到FSM模型的转换,给出了各自的转换方法,并实现了原型工具UML2FSM.     

Timing consistency checking for UML/MARTE behavioral models

UML/MARTE model-driven development approaches are gaining attention in developing real-time embedded software (RTES). UML behavioral models with MARTE annotations are used to describe timing behaviors and timing characteristics of RTES. Particularly, state machine, sequence, and timing diagrams with MARTE annotations are appropriate to understand and analyze timing behaviors of RTES. However, to guarantee software correctness and safety, timing inconsistencies in UML/MARTE should be identified in the design phase of RTES. UML/MARTE timing inconsistencies are related to modeling errors and can be hazards throughout the lifecycle of RTES. We propose a systematic approach to check timing consistency of state machine, sequence, and timing diagrams with MARTE annotations for RTES. First, we present how state machine, sequence, and timing diagrams with MARTE annotations specify the behaviors of RTES. To overcome informal semantics of UML/MARTE models, we provide formal definitions of state machine, sequence, and timing diagrams with MARTE annotations. Second, we present the timing consistency checking approach that consists of a rule-based and a model checking-based timing consistency checking. In the rule-based timing consistency checking, we validate well formedness of UML/MARTE behavioral models in timing aspects. In the model checking-based timing consistency checking, we verify whether timing behaviors of sequence and timing diagrams with MARTE annotations are consistent with the timing behaviors of state machine diagrams with MARTE annotations. We support an automated timing consistency checking tool UML/MARTE timing Consistency Analyzer for a seamless approach. We demonstrate the effectiveness and the practicality of the proposed approach by two case studies using cruise control system software and guidance and control unit software.     

基于UML的医院信息系统建模

UML是一种面向对象的建模语言,能够将用户的业务需求映射为模型,可大大提高系统的开发效率和扩展性。运用UML用例图、时序图、协作图、状态图、活动图等表示方法,对医院信息系统HIS的需求和业务流程进行分析与设计,准确地表达系统的功能需求,有效解决了HIS的需求分析和业务建模问题,为下一步的总体设计奠定了良好的基础。     

Synthesizing object life cycles from business process models

Unified modeling language (UML) activity diagrams can model the flow of stateful business objects among activities, implicitly specifying the life cycles of those objects. The actual object life cycles are typically expressed in UML state machines. The implicit life cycles in UML activity diagrams need to be discovered in order to derive the actual object life cycles or to check the consistency with an existing life cycle. This paper presents an automated approach for synthesizing a UML state machine modeling the life cycle of an object that occurs in different states in a UML activity diagram. The generated state machines can contain parallelism, loops, and cross-synchronization. The approach makes life cycles that have been modeled implicitly in activity diagrams explicit. The synthesis approach has been implemented using a graph transformation tool and has been applied in several case studies.