Clock constraint specification language: specifying clock constraints with UML/MARTE

The Object Management Group (OMG) unified modeling language (UML) profile for modeling and analysis of real-time and embedded systems (MARTE) aims at using the general-purpose modeling language UML in the domain of real-time and embedded (RTE) systems. To achieve this goal, it is absolutely required to introduce inside the mainly untimed UML an unambiguous time structure which MARTE model elements can rely on to build precise models amenable to formal analysis. The MARTE Time model has defined such a structure. We have also defined a non-normative concrete syntax called the clock constraint specification language (CCSL) to demonstrate what can be done based on this structure. This paper gives a brief overview of this syntax and its formal semantics, and shows how existing UML model elements can be used to apply this syntax in a graphical way and benefit from the semantics.     

Institutionalising UML 2.0 state machines

A key challenge to achieve a unified semantics for UML is how to handle the heterogeneity of its sublanguages. In this context, the theory of institutions provides an elegant and robust framework for programming in the large and in particular for compositionality. It can be used to define a family of formalisms which capture various UML sublanguages, and morphisms that represent the expected semantic relationships between them, resulting in a heterogeneous environment for the semantic definition of UML. The main goal of this work is to collaborate with the definition of such environment. For this purpose, we define an institution for UML 2.0 state machines. The building blocks of our institution are based on a previous semantics dealing with processing simple input events within a transition step. We also extend these semantic definitions for handling sequences of events, and then for considering runs through the state machine.     

Using UML Action Semantics for model execution and transformation

The Unified Modelling Language (UML) lacks precise and formal foundations and semantics for several modeling constructs, such as transition guards or method bodies. These semantic discrepancies and loopholes prevent executability, making early testing and validation out of reach of UML tools. Furthermore, the semantic gap from high-level UML concepts to low-level programming constructs found in traditional object-oriented language prevents the development of efficient code generators.The recent Action Semantics (AS) proposal tackles these problems by extending the UML with yet another formalism for describing behavior, but with a strong emphasis on dynamic semantics. This formalism provides both, a metamodel integrated into the UML metamodel, and a model of execution for these statements. As a future OMG standard, the AS eases the move to tool interoperability, and allows for executable modeling and simulation.We explore in this paper a specificity of the AS: its applicability to the UML metamodel, itself a UML model. We show how this approach paves the way for powerful metaprogramming for model transformation. Furthermore, the overhead for designers is minimal, as mappings from usual object-oriented languages to the AS will be standardized.     

A real-time profile for UML

This paper describes an approach for real-time modelling in UML, focusing on analysis and verification of time and scheduling-related properties. To this aim, a concrete UML profile, called the ωprofile, is defined, dedicated to real-time modelling by identifying a set of relevant concepts for real-time modelling which can be considered as a refinement of the standard SPT profile. The profile is based on a rich concept of event representing an instant of state change, and allows the expression of duration constraints between occurrences of events. These constraints can be provided in the form of OCL-like expressions annotating the specification or by means of state machines, stereotyped as ‘observers’. A framework for modelling scheduling issues is obtained by adding a notion of resource and a notion of execution time. For proving the relevance of these choices, the profile has been implemented in a validation tool and applied to case studies. It has a formal semantics and is sufficiently general and expressive to define a semantic underpinning for other real-time profiles of UML which in general define more restricted frameworks. In particular, most existing profiles handling real-time issues define a number of predefined attributes representing particular durations or constraints on them and their semantic interpretation can be expressed in the OMEGA-RT profile. This work has been partially supported by the IST-2002-33522 OMEGA project. VERIMAG is an academic research laboratory associated with CNRS, Université Joseph Fourier and Institut Nationale Polytechnique de Grenoble.     

An integrated semantics for reasoning about SysML design models using refinement

SysML is a variant of UML for systems design. Several formalisations of SysML (and UML) are available. Our work is distinctive in two ways: a semantics for refinement and for a representative collection of elements from the UML4SysML profile (blocks, state machines, activities, and interactions) used in combination. We provide a means to analyse and refine design models specified using SysML. This facilitates the discovery of problems earlier in the system development lifecycle, reducing time, and costs of production. Here, we describe our semantics, which is defined using a state-rich process algebra and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case study is a leadership-election protocol, a critical component of an industrial application. Our major contribution is a framework for reasoning using refinement about systems specified by collections of SysML diagrams.     

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.     

A cognitive semantics for the association construct

The unified modelling language (UML), besides its traditional use in describing software artifacts, is increasingly being used for conceptual modelling, the activity of describing an application domain. For models to be clear and unambiguous, every construct of the modelling language must have well-defined semantics, which is its mapping to elements of the semantic domain. When used for conceptual modelling, the semantic domain of UML is the application domain, as perceived by the modeller. Modellers perceive and structure their perceptions using cognitive concepts. This paper proposes a mapping of the UML association construct to those concepts. Implications for the use of the association construct for conceptual modelling are derived, a UML profile for conceptual modelling is presented, along with the results of a case study using the semantics and profile.

Dynamic Meta Modeling with time: Specifying the semantics of multimedia sequence diagrams

The Unified Modeling Langugage (UML) offers different diagram types to model the behavior of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time in behavioral models since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain.We have proposed Dynamic Meta Modeling (DMM), an approach based on graph transformation, as a means for specifying operational semantics of dynamic UML diagrams. In this article, we extend this approach to also account for time by extending the semantic domain to timed graph transformation. This enables us to define the operational semantics of UML diagrams with time specifications. As an example, we provide semantics for special sequence diagrams from the domain of multimedia application modeling.     

The many meanings of UML 2 Sequence Diagrams: a survey

Scenario languages are widely used in software development. Typical usage scenarios, forbidden behaviors, test cases, and many more aspects can be depicted with graphical scenarios. Scenario languages were introduced into the Unified Modeling Language (UML) under the name of Sequence Diagrams. The 2.0 version of UML changed Sequence Diagrams significantly and the expressiveness of the language was highly increased. However, the complexity of the language (and the diversity of the goals Sequence Diagrams are used for) yields several possible choices in its semantics. This paper collects and categorizes the semantic choices in the language, surveys the formal semantics proposed for Sequence Diagrams, and presents how these approaches handle the various semantic choices.     

Dynamic Meta Modeling with Time: Specifying the Semantics of Multimedia Sequence Diagrams

UML offers different diagram types to model behavior and dynamics of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain. We have proposed Dynamic Meta Modeling (DMM) as a means for the specification of the formal operational semantics of UML models by applying graph transformation to the meta modeling of dynamic behavior. Within this paper, we extend this approach to also account for time by building on timed graph transformations. We apply these concepts to the domain of multimedia application modeling in which we adopt UML sequence diagrams. The DMM rules with time then specify an interpreter that can be used to analyze or test a model of multimedia sequence diagrams.     

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.     

基于XML的UML模型向AADL模型的自动转换

UML已经成为复杂系统建模的工业标准,并可借助代码自动生成工具实现从分析到编码的开发过程自动化;AADL具有精确的语义和严格的语法规范,可用于描述嵌入式实时系统的软、硬件体系结构,并能分析系统的功能及非功能属性。 UML和AADL模型的基本元对象有相互对应关系,并且两种模型的表示都能够采用标准的XML的交换格式。为充分发挥两种语言的优势,文中研究了UML模型向AADL模型的自动转换,以XML为媒介实现两种模型的元对象的对应转换,最终达到两种模型的转换,使用户在设计阶段能够结合运用AADL、UML工具的优点对系统进行分析。     

VPM: A visual,precise and multilevel metamodeling framework for describing mathematical domains and UML (The Mathematics of Metamodeling is Metamodeling Mathematics)

As UML 2.0 is evolving into a family of languages with individually specified semantics, there is an increasing need for automated and provenly correct model transformations that (i) assure the integration of local views (different diagrams) of the system into a consistent global view, and, (ii) provide a well-founded mapping from UML models to different semantic domains (Petri nets, Kripke automaton, process algebras, etc.) for formal analysis purposes as foreseen, for instance, in submissions for the OMG RFP for Schedulability, Performance and Time. However, such transformations into different semantic domains typically require the deep understanding of the underlying mathematics, which hinders the use of formal specification techniques in industrial applications. In the paper, we propose a multilevel metamodeling technique with precise static and dynamic semantics (based on a refinement calculus and graph transformation) where the structure and operational semantics of mathematical models can be defined in a UML notation without cumbersome mathematical formulae.     

Specification of Real-Time Systems in UML

We introduce time semantics into UML class and statechart diagrams. This extends the expressiveness of UML for specification of real-time systems and allows to specify verification properties of real-time systems by means of Timed Computation Tree Logic. We furthermore propose a way to collect stereotypes for specification of real-time systems. The approach is illustrated by a case study.     

基于本体的UML类图语义推理

统一建模语言(UML)是一个半形式化的语言,其语义部分是采用自然语言描述的,使得它在建模过程中会产生语义不一致等问题。在详细比较UML类图与本体的基础上,提出了一种UML类图的形式化方法;首先将UML类图转换为相应的本体;然后根据本体提供的推理算法(Tableau)对转换得到的本体进行推理,检测其中的不一致性从而修改UML类图,最后达到精确UML类图。     

Polymorphic scenario-based specification models: semantics and applications

We present polymorphic scenarios, a generalization of a UML2-compliant variant of Damm and Harel??s live sequence charts (LSC) in the context of object-orientation. Polymorphic scenarios are visualized using (modal) sequence diagrams where lifelines may represent classes and interfaces rather than concrete objects. Their semantics takes advantage of inheritance and interface realization to allow the specification of most expressive, succinct, and reusable universal and existential inter-object scenarios for object-oriented system models. We motivate the use of polymorphic scenarios, formally define their trace-based semantics, and present their application for scenario-based testing and execution, as implemented in the S2A compiler developed at the Weizmann Institute of Science. We further discuss advanced semantic issues arising from the use of scenarios in a polymorphic setting, suggest possible extensions, present a UML profile to support polymorphic scenarios, consider the application of the polymorphic semantics to other variants of scenario-based specification languages, and position our work in the broader context of behavioral subtyping.     

A UML-based static verification framework for security

Secure software engineering is a new research area that has been proposed to address security issues during the development of software systems. This new area of research advocates that security characteristics should be considered from the early stages of the software development life cycle and should not be added as another layer in the system on an ad-hoc basis after the system is built. In this paper, we describe a UML-based Static Verification Framework (USVF) to support the design and verification of secure software systems in early stages of the software development life-cycle taking into consideration security and general requirements of the software system. USVF performs static verification on UML models consisting of UML class and state machine diagrams extended by an action language. We present an operational semantics of UML models, define a property specification language designed to reason about temporal and general properties of UML state machines using the semantic domains of the former, and implement the model checking process by translating models and properties into Promela, the input language of the SPIN model checker. We show that the methodology can be applied to the verification of security properties by representing the main aspects of security, namely availability, integrity and confidentiality, in the USVF property specification language.