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

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

基于UML的嵌入式系统建模及模型验证机制研究

统一建模语言UML在嵌入式系统设计建模中已经获得了广泛的认可，并有很多成功的应用，但UML存在时间约束描述能力不强和所建模型形式化复杂、验证难的问题。针对上述问题，本文提出了使用UML扩展机制对UML状态图进行时间扩展，建立系统状态一约束一事件矩阵来对模型进行形式化描述的方法。该方法解决了UML在嵌入式系统建模时存在的问题。应用实例和实验结果验证了该方法的可行性和有效性。     

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

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

基于UML的嵌入式系统模型验证机制的研究

随着嵌入式系统在各个领域的广泛应用,嵌入式系统变得越来越复杂,研究一种支持嵌入式系统从分析、设计、验证到编码这一整个开发过程的模型系统及建模方法变得越来越重要。UML(UnifiedModelingLanguage,统一建模语言)作为面向对象的分析与设计技术的代表,已经获得了广泛的承认,并在多个领域中有成功的应用。然而,UML是一种符号化语言系统,其语义采用自然语言描述,没有完全形式化,无法精确和严格地描述模型的行为从而实现模型的验证。为了解决这个问题,文章提出了一种用于嵌入式系统UML模型验证的方法,其核心是可执行(Executable)UML,它是UML的增强性子集,采用与UML相同的符号表示法,并集成了状态图(StateChart)所用的形式化语义定义。嵌入式系统的UML模型经过语义分析能够很方便地生成可执行UML模型,并实现系统模型的验证。     

基于状态图的对象行为建模

状态图（State Chart）是对对象的行为的一种描述的方法,并是UML（Unified Modeling Language）可视化建模的一部分。文中分析了状态图建模的规则,以及如何用状态图对对象的行为进行建模的方法。     

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

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

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

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

基于Petri网的UML形式化建模应用分析

UML是功能强大的图形化建模语言,但存在缺乏精确的语义描述的特点,因此UML形式化研究一直是一个热点。Petri网既有直观的图形表示,又有坚实的数学基础,拥有许多成熟的分析方法可以直接用于分析模型的性能。结合一个图录编纂应用系统,使用基于Petri网的建模方法,对该系统的UML状态图和序列图进行了形式化分析。排除UML模型中的缺陷,在软件设计阶段发现错误,降低软件开发的花销,最终达到提高了软件的质量的目的。     

基于动态描述逻辑的UML状态图形式化方法

统一建模语言(UML)状态图包括静态语义和动态语义.针对该特点,提出基于动态描述逻辑的UML状态图形式化方法,介绍动态描述逻辑DDL_SHOIN(D)的语法和语义,设计UML状态图的DDL_SHOIN(D)形式化方法,研究状态图动作推理问题.给出状态图状态可达性和动作包含关系的定义,并证明其正确性.     

UML状态图形式化方法的分析与比较

UML缺乏精确的语义,难以对其所表示的系统进行形式化分析和一致性检验.为了使UML能够更精确地对系统模型进行描述,学者们提出了一些形式化的方法.论文对比分析了用Petri网、时序逻辑XYE/E和动态描述逻辑形式化UML状态图的方法,指出了它们各自的优缺点以及应用领域.     

基于Spin的UML状态图模型检查的设计与实现

UML已经是软件建模方面的标准语言,UML Statechart描述了系统在其生命周期中的动态行为。随着系统规模的扩大和复杂度的提高,Statechart往往包含设计者所未预料到的隐患,通过模型检查来对Statechart进行穷举检验就成为一个重要课题,首先给出了含层次、并发Statechart的语义;随后提出了对Statechart进行模型检查的一种新方法,并且已经编写软件SC2Spin实现此方法,该方法使用了提出的Statechart山脉算法和迁移提取法,可以将一个Statechart自动转化为Spin的输入语言Promela,从而验证Statechart的死锁、活锁等错误和时序逻辑公式。     

扩展UML状态图在软件测试中的应用

在可测试性方面，UML状态图模型存在不完整性和二义性及结构复杂不便于状态分析等缺陷。该文讨论了基于扩展UML状态图模型的测试用例生成技术，分析了基于扩展UML状态图模型的测试用例生成技术。针对UML状态图的不完整性和二义性进行扩展，以提高其可测试性。     

基于UML Statechart语义的测试序列生成方法

UML Statechart是UML的一个主要组成部分,与其他类型的Statechart相比,由于采用事件队列的调度方式,UML Statechart有着更多的不确定性,使得针对UML Statechart 模型的测试非常困难。本文给出了一个形式化的语义模型,并将Stateehart转化为一个比较简单的标志变迁系统,利用路径选择算法得到一个基于标志变迁系统的测试集,然后通过判断得到的测试集中每个测试用例是否满足UML Statechart执行步的语义,从而得到一个满足UML Statechart执行步的语义的、可执行的测试集。     

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     

Using a process algebra interface for verification and validation of UML statecharts

UML diagrams are the conventional methods for visual modeling systems. Among them, the Statechart diagrams are used to show the runtime behavior of a system, but the correctness of such diagrams is the primary concern of the designers because of concurrency issues like livelock, inaccessible states, and non-deterministic states. Process algebra methods have the capabilities that are suitable for verification and validation of Statecharts. To this end, in this paper, process algebra language LOTOS (Language Of Temporal Ordering Specification) is used as the target language, and a method is presented to map UML Statecharts to the LOTOS processes, called USLP. Then the correctness of the proposed mappings is proved by demonstrating the isomorphism relation between the Labeled Transition System (LTS) of a Statechart and the LTS of its transformed LOTOS specification. Next, tools CADP (Construction and Analysis of Distributed Processes) is used for verification and validation of the mapped LOTOS models, and the CSP process algebra and its tools, FDR are used to verify the properties could not be verified by the LOTOS and its toolset. The experimental results show our approach can: (1) verify some properties (the issues) that are not verified by other approaches and (2) reduce the space that should be searched to verify the properties.     

基于扩展UML statecharts的协议测试

提出了一种基于扩展UML statecharts的协议一致性测试方法.实时扩展使得UML statecharts可直接描述时间约束,方便进行一致性测试;以FREE(Flattened Regular Expression)模型图为基础生成抽象测试序列,然后根据时间覆盖准则,生成实时测试序列.     

Automated Prototyping of User Interfaces Based on UML Scenarios

User interface (UI) prototyping and scenario engineering have become popular techniques. Yet, the transition from scenario to formal specifications and the generation of UI code is still ill-defined and essentially a manual task, and the two techniques lack integration in the overall requirements engineering process. In this paper, we suggest an approach for requirements engineering that generates a user interface prototype from scenarios and yields a formal specification of the application. Scenarios are acquired in the form of collaboration diagrams as defined by the Unified Modeling Language (UML), and are enriched with user interface (UI) information. These diagrams are automatically transformed into UML Statechart specifications of the UI objects involved. From the set of obtained specifications, a UI prototype is generated that is embedded in a UI builder environment for further refinement. Based on end user feedback, the collaboration diagrams and the UI prototype may be iteratively refined, and the result of the overall process is a specification consisting of the Statechart diagrams of all the objects involved, together with the generated and refined prototype of the UI. The algorithms underlying this process have been implemented and exercised on a number of examples. This research was mainly conducted at University of Montreal, where the first two authors were PhD students and the third author a full-time faculty member. Funding was provided in part by FCAR (Fonds pour la formation des chercheurs et l'aide à la recherche au Québec) and by the SPOOL project organized by CSER (Consortium Software Engineering Research) which is funded by Bell Canada, NSERC (Natural Sciences and Research Council of Canada), and NRC (National Research Council Canada).     

The UML as a formal modeling notation

The Unified Modeling Language (UML) is an Object Management Group (OMG) object-oriented (OO) modeling notation standard. It consists of a set of notations for modeling systems from a variety of views and at varying levels of abstraction. While the UML reflects some of the best OO modeling experiences available, it suffers from a lack of precise semantics that is necessary if one is to use the notations to precisely model systems and to rigorously reason about the models. In this paper we discuss some of the problems with the current UML semantic document and present the approach that the precise UML group (pUML) group is using to develop a precise semantics for the UML. The approach utilizes mathematical techniques to explore and gain insights into appropriate semantics for UML modeling concepts. The insights and formal expressions will then be used to develop a UML semantics document written in natural language that defines the semantics in a precise, consistent, and understandable manner.     

Exploiting Visual Languages Generation and UML Meta Modeling to Construct Meta-CASE Workbenches

In the paper we propose an approach for the construction of meta-CASE workbenches. The approach is based on the technology of visual language generation systems and on UML meta modeling. Visual modeling environments are generated starting from UML class diagrams specifying abstract syntax of the underlying visual language. The meta-CASE generates a workbench by integrating a set of visual modeling environments through inter-consistency constraints defined on the corresponding UML class diagrams.     

基于一致性测试理论的Statechart描述的测试用例自动生成

本文研究Statechart描述的测试语义和测试用例的自动生成.基于Tretmans的从标记转换系统描述自动生成测试用例的方法,我们研究如何从Statechart描述自动生成测试用例.本文的主要贡献在于建立了基于Statechart描述的一致性测试和测试用例生成的形式化基础.为Statechart描述建立了形式化测试语...