UML顺序图的自动验证

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

面向并行工程的组合夹具辅助设计系统设计与开发

提出了一种基于Web的计算机辅助夹具设计系统原型,并采用基于UML的ICONIX开发过程实现,通过用例图、对象类图、Robustness图和顺序图明确了系统对象类的功能、关联以及协同关系．     

基于UML活动图生成系统测试场景的方法

旨在研究运用统一建模语言（UML）活动图生成测试场景的方法。首先对UML活动图进行了形式化定义,确定了一系列覆盖准则。然后,根据覆盖准则制定活动图的一般处理思路,针对活动图中并发结构提出采用信号量和嵌套分割的方法进行处理。该方法有效控制了测试场景集的数量,为UML活动图的自动化测试提供了系统的、有效的、可行的方法。     

UML Statecharts的模型检验方法

统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Büchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统.     

基于UML活动图的系统测试方法研究

研究以统一建模语言UML分析设计模型进行系统测试的方法.为了从UML设计模型中的活动图生成测试场景,给出了UML活动图的形式化定义和基路径方法.由于活动图中并发活动单入单出的性质,对并发活动进行压缩,用基路径方法找出其中的基路径,然后替换并发活动生成完整的测试场景.为了避免场景数量爆炸,文中对活动图的循环和并发进行了约束.最后讨论了从测试场景生成测试用例的方法,并通过一个实例说明了应用本方法的可行性和有效性.     

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

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

基于UML的软硬件协同设计方法

嵌入式系统软硬件协同设计中关键步骤之一是软硬件划分。文中通过介绍现有嵌入式系统的协同设计方法，如：VULCAN，COSYMA和POLLS，指出了现有方法的缺点，提出了一种改进的基于UML的新方法。使用UML建立系统模型，根据UML的图例，采用二叉树的结构，计算出每个步骤的成本；采用改进的遗传算法，加快收敛的速度，提高解的质量。在算法库和成本库中对系统的软硬件进行划分，通过协同综合，达到协同仿真和验证的目的。     

基于UML和RUL设计高职院校教务管理系统的研究

随着职业化教育改革的不断推进,高校教务管理工作量大幅度增加,其复杂性也越来越大。这使得高校教务管理工作的信息化和网络化势在必行。与此同时,校园网的建立和Internet技术的引进为建立这样的系统提供了必要的条件。因此,该文针对高职院校的教务管理模式开发基于校园网的教务管理系统。该文使用UML统一建模语言和Rational统一过程对高职学院院校管理系统进行系统设计。在本论文中详细讨论的系统的需求分析,使用UML建模语言分析了管理系统的用例。以用例图为基础,进一步分析系统。使用对象图,协同图等表达系统对象之间的管理。开发系统的过程中,我们针对本系统客户端众多的特点,采用了以B/S模式为主,C/S模式为辅的开发模式。为了得到良好的伸缩性,结合COM+技术,采用三层体系结构开发。     

基于UML扩展的实时系统建模方法

UML是一种应用广泛的面向对象建模语言,但是在对实时系统的建模中,UML缺乏实时和并发特性的描述能力,运用UML的扩展机制,借鉴着色Petri网描述并发的思想,扩充了UML的模型元素,并在此基础上提出了一种并发图,用于描述实时系统任务间的动态并发行为。最后通过一个实例说明了该扩展的应用方法和有效性。     

UML在生产管理信息系统中的应用

本文以生产管理信息系统为研究对象,利用UML,对系统的实现进行了需求和问题领域分析,建立了静态、动态行为模型、对象类图及物理实现构件图,对UML的建模机制作了系统的概述,实现了生产管理信息系统实现一个比较完整的过程.     

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

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

Formalising concurrent UML state machines using coloured Petri nets

With the increasing complexity of dynamic concurrent systems, a phase of formal specification and formal verification is needed. UML state machines are widely used to specify dynamic systems behaviours. However, the official semantics of UML is described in a semi-formal manner, which renders the formal verification of complex systems delicate. In this paper, we propose a formalisation of UML state machines using coloured Petri nets. We consider in particular concurrent aspects (orthogonal regions, forks, joins, variables), the hierarchy induced by composite states and their associated activities, external, local or inter-level transitions, entry/exit/do behaviours, transition priorities, and shallow history pseudostates. We use a CD player as a motivating example, and run various verifications using CPN Tools.     

Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker

Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency. Received September 1999 / Accepted in revised form February 2000     

一种基于面向侧面技术的并发式软件建模方法

基于面向侧面（Aspect-Oriented）技术及统一建模语言状态图提出了并发式软件系统开发过程中横切特性的建模方法。本方法将并发软件系统的业务逻辑和横切行为分别封装到复合状态的不同正交区域中，并通过事件广播机制反映二者的交互关系。同时，以模块化的状态迁移系统 （Modular Transition System）作为基本计算模型，对该建模方法进行形式化描述，给出了模型元素及建模过程的精确语义。实例研究表明，该方法在并发软件设计阶段实现了横切关注点的分离策略，并使得系统模型具有松耦合、适应性和可跟踪性的优点。     

Does aspect-oriented modeling help improve the readability of UML state machines?

Aspect-oriented modeling (AOM) is a relatively recent and very active field of research, whose application has, however, been limited in practice. AOM is assumed to yield several potential benefits such as enhanced modularization, easier evolution, increased reusability, and improved readability of models, as well as reduced modeling effort. However, credible, solid empirical evidence of such benefits is lacking. We evaluate the “readability” of state machines when modeling crosscutting behavior using AOM and more specifically AspectSM, a recently published UML profile. This profile extends the UML state machine notation with mechanisms to define aspects using state machines. Readability is indirectly measured through defect identification and fixing rates in state machines, and the scores obtained when answering a comprehension questionnaire about the system behavior. With AspectSM, crosscutting behavior is modeled using so-called “aspect state machines”. Their readability is compared with that of system state machines directly modeling crosscutting and standard behavior together. An initial controlled experiment and a much larger replication were conducted with trained graduate students, in two different institutions and countries, to achieve the above objective. We use two baselines of comparisons—standard UML state machines without hierarchical features (flat state machines) and standard state machines with hierarchical/concurrent features (hierarchical state machines). The results showed that defect identification and fixing rates are significantly better with AspectSM than with both flat and hierarchical state machines. However, in terms of comprehension scores and inspection effort, no significant difference was observed between any of the approaches. Results of the experiments suggest that one should use, when possible, aspect state machines along with hierarchical and/or concurrent features of UML state machines to model crosscutting behaviors.     

基于并行对象的可视化模型

提出了一种基于并行对象的可视化模型,该模型中吸取了数据流图、Petri-net和UML技术中的基本思想,通过使用数据流图来确定数据加工状态,从而初步得到并行对象的雏形,然后使用Petri-net来描述并行对象的动态特征,最后使用UML对并行对象的静态信息进行描述。通过静态描述和动态描述自动为用户生成并行程序的代码框架。     

Concurrency and Refinement in the Unified Modeling Language

This paper shows how a formal notion of refinement may be defined for models, and model components, expressed in the Unified Modeling Language (UML). A formal, behavioural semantics is given to combinations of class, object, and state diagrams, using the notation of Communicating Sequential Processes (CSP); this semantics is adequate for the analysis of concurrent, communicating behaviour, and induces a notion of refinement for UML based upon existing notions of traces and failures refinement for CSP.     

基于UML状态图的软件测试研究

UML状态图与传统的状态转换图存在较大的差异,导致由状态转换图得到的软件测试路径不适用于UML状态图。为此,提出一种由UML状态图得到软件测试路径的方法。通过对UML状态图逐层分析,并将并发子状态相互组合,以获得状态迁移路径,从而得到软件测试路径。实例证明,该方法可以从UML状态图得出软件的测试路径。     

A state/event-based model-checking approach for the analysis of abstract system properties

We present the UMC framework for the formal analysis of concurrent systems specified by collections of UML state machines. The formal model of a system is given by a doubly labelled transition system, and the logic used to specify its properties is the state-based and event-based logic UCTL. UMC is an on-the-fly analysis framework which allows the user to interactively explore a UML model, to visualize abstract behavioural slices of it and to perform local model checking of UCTL formulae. An automotive scenario from the service-oriented computing (SOC) domain is used as case study to illustrate our approach.