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

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

UML活动图的时序逻辑语义

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

基于时序逻辑的UML2.0通信图语义研究

UML2.0通信图可以表示对象之间的交互,很适合用于对系统的交互行为建模,但由于UML缺乏精确语义,使得难以对其所表示的系统行为进行分析和验证.XYZ/E是可执行线性时序逻辑语言,既可描述系统的静态语义和动态语义.在定K.UML2.0通信图的形式化语法的基础上,给出了通信图的XYZ/E时序逻辑语义,为进一步的系统分析和验证提供了形式化基础.     

基于UML和XYZ/E的ATM系统体系结构描述

本文提出了将可视化建模语言UML和时序逻辑语言XYZ/E相结合来描述软件体系结构的方法。首先给出了该方法的基本框架,然后对XYZ/E进行扩展,使之能够显式地表示软件体系结构的基本元素,并定义了UML活动图的形式语义,最后,通过银行ATM实例进一步说明了该方法的可行性,对可视化和形式化相结合描述软件体系结构的研究具有一定的推动作用。     

UML类图的形式化及分析

统一建模语言(UML)是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为事实上的工业标准。但是UML不是形式化的建模语言,缺乏精确的语义描述,因此会导致一些问题。Z是一种广泛使用的形式化规约语言,Z适合用来精确地表示模型的语法和语义。文章采用Z符号来表示UML类图的组成元素的语法和语义及其映射关系,最后对UML类图的一些性质进行分析和验证。     

UML状态机模型元素的RSL形式化定义

UML状态机作为UML动态描述机制的重要组成部分,在描述系统及模型的动态行为时扮演着重要的角色,但已有的UML动态语义缺乏准确的形式化描述。首先将UML状态机抽象成图;再将图通过传统的有穷自动机进行语义扩展,同时增加状态分层,形成一个基于UML状态机的有穷自动机;然后用RAISE规约语言RSL对扩展后的自动机进行形式化定义,使UML状态机中的模型元素的语义更加清晰、精确,为后期的UML状态机的操作语义形式化研究打下基础。     

体系结构描述语言XYZ/ADL到UML的映射

选择了一种基于时序逻辑语言XYZ/E的体系结构描述语言XYZ/ADL,分析了其设计元素和UML建模元素的语义,并通过UML扩展机制和对象约束语言进行扩展和约束,建立起从XYZ/ADL到UML的映射。     

UML活动图的操作语义

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

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

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

基于线性时序逻辑的实时系统建模与求精

线性时序逻辑语言XYZ／E在统一的语义框架下．能表示从高层需求规范到低层实现模型之间的不同抽象层次的系统描述，也适于描述实时系统的模型和逐步求精过程．本文提出了一种基于构件的实时系统求精方法，并给出一个具体实例一电梯控制系统，采用XYZ／E语言描述了该系统的模型及其求精过程．     

Graphic Language for Describing Constraints on Diagrams of UML Classes

A visual notation for specifying constraints on diagrams of UML classes by means of the UML collaboration diagrams is suggested. A formal semantics of the suggested notation is presented.     

TURTLE: a real-time UML profile supported by a formal validation toolkit

We present a UML 1.5 profile named TURTLE (Timed UML and RT-LOTOS Environment) endowed with a formal semantics given in terms of RT-LOTOS. TURTLE relies on UML's extensibility mechanisms to enhance class and activity diagrams. Class diagrams are extended with specialized classes named Tclasses, which communicate and synchronize through gates. Also, associations between Tclasses are attributed by a composition operator (Parallel, Synchro, Invocation, Sequence, or Preemption) which provides them with a formal semantics. TURTLE extends UML activity diagrams with synchronization actions and temporal operators (deterministic delay, nondeterministic delay, time-limited offer, and time-capture). The real-time dimension of TURTLE has been further improved by the addition of two composition operators, periodic and suspend, as well as suspendable delay, latency, and time-limited offer operators at the activity diagram level. Core characteristics of TURLE are supported by TTool - the TURTLE toolkit - which includes a diagram editor, a RT-LOTOS code generator and a result analyzer. The toolkit reuses RTL, a RT-LOTOS validation tool offering debug-oriented simulation and exhaustive analysis. TTool hides RT-LOTOS to the end-user and allows him/her to directly check TURTLE modeling against logical errors and timing inconsistencies. Besides the foundations of the TURTLE profile, this paper also discusses its application in the context of space-based embedded software.     

UML2.0顺序图的形式化研究

在UML2.0规范中顺序图的语义仍然是以自然语言的形式描述的,为实现对顺序图的自动化分析和验证,必须为顺序图定义一种形式化的语义模型.为此首先给出了UML顺序图的一种符合BNF范式的形式化语法,然后为该语法中的非终止符定义转换规则,将UML顺序图中的基本动作转换为加标Petri网组件,最后定义了各种合成操作,利用这些合成操作可以将UML顺序图的加标Petri网组件转换为加标Petni网.     

A compositional semantics of UML-RSDS

This paper provides a semantics for the UML-RSDS (Reactive System Development Support) subset of UML, using the real-time action logic (RAL) formalism. We show how this semantics can be used to resolve some ambiguities and omissions in UML semantics, and to support reasoning about specifications using the B formal method and tools. We use ‘semantic profiles’ to provide precise semantics for different semantic variation points of UML. We also show how RAL can be used to give a semantics to notations for real-time specification in UML. Unlike other approaches to UML semantics, which concentrate on the class diagram notation, our semantic representation has behaviour as a central element, and can be used to define semantics for use cases, state machines and interactions, in addition to class diagrams.     

UML的形式化描述语义

本文提出了一种新的定义UML形式化语义的方法。我们将建模语言的语义区分为描述语义和功能语义两个方面。描述语义定义哪些系统满足模型,功能语义定义模型中的基本概念。本文用一阶逻辑定义了UML的类图、交互图和状态图的描述语义,并介绍我们实现的将UML模型转换成逻辑系统的软件工具LAMBDES,该工具集成了定理证明器SPASS,可以对模型进行自动推理。我们成功地将此方法和工具应用于模型的一致性检查。     

Concurrency and Refinement in the Unified Modeling Language

This paper defines a formal semantics for a subset of the Unified Modeling Language (UML). It shows how suitable combinations of class, object, state, and sequence diagrams can be associated with patterns of interaction, expressed in the event notation of Communicating Sequential Processes (CSP). The diagram semantics is then extended to give a meaning to complete models – suitable combinations of diagrams – and thus a concurrency semantics for object models written in UML. This model semantics is in turn used to define a theory of refinement, based upon existing notions of data and process refinement.     

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顺序图描述完整的C语言执行过程,将其形式化描述,实验结果表明,这种方法是可行的.