Presentations (Hosts)

 

Introducation (pdf) & System Model (pdf)

Bernhard Rumpe, Technical University of Braunschweig

An introduction to our system model, both the structural and control parts.

 

Mapping Class Diagrams to the System Model (pdf)

Juergen Dingel, Queen's University

A discusson of UML 2 class diagrams and how they can be mapped to our system model.

 

Actions - Overview and Mapping (pdf)

Michelle L. Crane, Queen's University

A discussion of UML 2 actions and how they can be mapped to our system model.

 

Activities - Overview and Mapping (pdf)

Michelle L. Crane, Queen's University

A discussion of UML 2 activities and how they can be mapped to our system model.

 

 

Abstracts & Presentations (Invited Speakers)


Defining Object-Oriented Execution Semantics Using Graph Transformations (pdf)

Anneke Kleppe, Harmen Kastenberg and Arend Rensink, University of Twente

In this presentation I describe an application of the theory of graph transformations to the practise of language design. In particular, we have defined the static and dynamic semantics of a small but realistic object-oriented language (called TAAL) by mapping the language constructs to graphs (the static semantics) and modelling their effect by graph transformation rules (the dynamic semantics). This gives rise to execution models for all TAAL-programs, which can be used as the basis for formal verification. This work constitutes a first step towards a method for defining all aspects of software languages, besides their concrete syntax, in a consistent and rigorous manner.

 

Analysis of UML Activities with Dynamic Meta Modeling Techniques (pdf)

Gregor Engels and Christian Soltenborn, University of Paderborn

Dynamic Meta Modeling(DMM) is a specification technique which allows to formally express the semantics of visual modeling languages. A DMM specification consists of the meta model of a language and a set of graph transformation rules: The former is mapped to a typed graph, the latter describes how that graph changes in time. This implies a transition system which can be used to analyze the behavior of the model. As a proof of concept we have applied the described approach to verify UML Activities for soundness, i.e., for well-defined termination. We have formalized soundness in the context of Activities and then utilized the GROOVE tool set to compute the transition systems of concrete Activities and to model check them for soundness.

 

An AsmL Semantics for Dynamic Structures in UML-RT (pdf)

Alin Stefanescu, Stefan Leue and Wei Wei, University of Konstanz

Most real-time systems employ runtime structural reconfiguration mechanisms based on dynamic creation and destruction of components and their relations. To support such features, the UML-RT profile provides a set of modeling concepts including optional actor roles, actor importation, multiple containment, and dynamic port connections. However these concepts are not covered in any of the current formal semantics of UML-RT, thus impeding the development of formal methods on UML-RT models. We use AsmL to present an executable semantics covering dynamic structures that facilitates the simulation and verification of UML-RT models using tools such as the Microsoft SpecExplorer tool supporting AsmL specifications. The formalization of dynamic structures in UML-RT may also improve our understanding of concepts newly introduced in UML 2.0, such as composite structures.

 

Template Semantics: Parameterized Semantics Descriptions (pdf)

Joanne Atlee, University of Waterloo

In this talk, I will describe a formalism we have developed, called template semantics, that structures the operational semantics of a family of notations as a set of predefined templates that must be instantiated with user-provided parameter values. Thus, thesemantics of a single notation can be described succinctly as a set of parameter values to this template. I will also talk about recent experiences in using this formalism to understand and compare notations.

 

A Formal Language for Specifying Models of Computations (pdf)

Gaston Christophe, CEA-LETI

Communicating-process-based systems are systems composed of several blocks, which are pieces of software or hardware continuously executing while interacting with other blocks of the system. We call processes such blocks. Modern communicating process based systems are often heterogeneous: processes composing such systems are described and implemented on specific particular models of time, of communication and of execution. Each block is designed and implemented in an independent manner but the way blocks are connected is generally treated at the code level. Designing such connections together with resulting intended behaviours requires defining a language dedicated to this purpose.

In the frame of the "Systematic" cluster (http://www.systematic-paris-region.org/) gathering industrials and academics of the "Ile-de-France" region in France, a project (PC_xUML) deals with this purpose. In this project we are defining a formal framework to be embedded in the UML to allow expressions of glues for heterogeneous processes. The framework has to be formal because it is the only way to define and evaluate correctness properties about model manipulations (e.g.: refinement, abstraction and structuring primitives). The motivations for choosing the UML are: * UML is the de facto standard language for modelling systems. * UML is by nature designed for supporting heterogeneous modelling: the UML is actually not a language but a family of languages. * We focus on processes described by using behavioural specification languages, that is: languages dedicated to describe executions rather than properties. Examples of such languages are: state machine, or more generally automata-based language, sequence diagram, or process algebra based language...This is because this kind of languages contains most of the usually used modelling languages in the industry. UML is suitable to describe such languages.

In this talk we will present the PC_xUML project, and discuss about possible collaboration schemas with other related initiatives.

 

BIP: Framework for Component Composition as a Means to Define Semantics (pdf)

Susanne Graf, VERIMAG

The talk defends the thesis that building a formal semantics that is on a side track with respect to valdiation and compilation tools is not helpful. The talk will also discuss structural features necessary for expressing a large variety of semantics, in particular concerning the interaction and execution modes. It will also present as proposal for such a framework.

 

A UML Simulator Based on a Generic Model Execution Engine (pdf)

Andrei Kirshin, IBM Haifa

We implemented a generic model execution engine. The engine provides mechanisms for the realization and the execution of behavioral semantics, and the control and observation of model behavior. We used this generic execution engine to implement a UML Model Simulator. It is designed as an extension to Rational Software Architect (RSA), adding execution and debugging capabilities. The current version of the UML Model Simulator supports UML classes and primitive data types, and focuses on the execution of activities and state machines. It also supports Java as an action language. Profiles can be used to add domain-specific behavior of a UML element, by applying stereotypes to UML elements. The tool can be extended to support the execution of models that conform to a specific profile.

The UML Model Simulator provides a wide range of debugging capabilities:

 

Queries and Constraints: A Comprehensive Semantic Model for UML2 (pdf)

Ingolf Krueger and Massimiliano Menarini, University of California, San Diego