Seminar: UML Foundations

News

The seminar usually takes place tuesdays from 16:00 to 17:00 at the seminar room of our chair
The slides of the first meeting (containg deadlines etc) are available here (the slides are in german).

First meeting: 13.02.2007, 16:00, Seminarraum Lehrstuhl Informatik 4 and not as mentioned earlier at Lehrstuhl für Informatik 2

Supervisors

Katoen
Noll
Ábrahám
Kern

Assignment of topics

Date	Student	Topic	Slides
03.04.2007	Ioannis Gatsioudis	Formal System Design Using Sequence Diagrams	---
10.04.2007	Christoph Güldenhofer	Timed and Probabilistic Sequence Diagrams	pdf
17.04.2007	Stefan Steinheimer	Live Sequence Charts	---
24.04.2007	Hector Diez-Cubeiro	Synthesis of state machines from Live Sequence Charts	pdf
02.05.2007	Christina Jansen	Theory of regular languages of Message Sequence Charts	pdf
08.05.2007	Christopher Lie	Semantics of sequence diagrams	ppt
15.05.2007	---	entfällt	---
22.05.2007	Fei Mo	UML Statechart semantics	ppt
12.06.2007	---	entfällt	---
05.06.2007	---	entfällt	---
19.06.2007	Ognyana Hristova	Timed UML state machines	ppt
26.06.2007 (16:00-17:00)	Abdallah Salim	Probabilistic and stochastic UML Statecharts	pdf
03.07.2007	Piotr Irla	Timed extensions of the OCL	ppt
10.07.2007	Dominik Franke	Model checking UML activity diagrams	---

Topic

Many international researchers and practitioners share the aim of developing the Unified Modeling Language (UML) as a precise (i.e. well defined) modeling language. This encompasses, amongst others:

to clarify and make precise the semantics of UML.
to reason with properties of UML models.
to verify the correctness of UML designs.

This seminar aims to obtain an overview of the current state-of-the art in providing a precise meaning to UML notations. The seminar focuses on UML statecharts to describe the functional behavior of systems, UML sequence diagrams for requirements specification, OCL (The Object Constraint Language) for specifying properties of UML models. The synthesis of first design models from sequence diagrams is also covered. Besides the various UML dialects, practical relevant variants of UML notations such as Stateflow will be treated as well.

Contact

If you have any question regarding the seminar please contact Carsten Kern.

Prerequisites

A "Vordiplom" or Bachelor in Computer Science. Knowledge on formal semantics is a beneficial, but not a must. Despite the topic is UML, the emphasis is on theory, and, e.g., not on the usage of the UML in the software development process.

Topics and Literature

1. Formal System Design Using Sequence Diagrams

Date:

Student:

Supervisor:

Literature:

Ragnhild Kobro Runde, Øystein Haugen, Ketil Stølen: The Pragmatics of STAIRS. FMCO 2005: 88-114 [pdf]
Øystein Haugen, Knut Eilif Husa, Ragnhild Kobro Runde, Ketil Stølen: STAIRS towards formal design with sequence diagrams. SoSym 355-367, 2005. [pdf]

2. Timed and Probabilistic Sequence Diagrams

Date:

Student:

Supervisor:

Literature:

Atle Refsdal, Knut Eilif Husa, Ketil Stølen: Specification and Refinement of Soft Real-Time Requirements Using Sequence Diagrams. FORMATS 2005: 32-48 [pdf]
Atle Refsdal, Ragnhild Kobro Runde, Ketil Stølen: Underspecification, Inherent Nondeterminism and Probability in Sequence Diagrams. FMOODS 2006: 138-155 [pdf]
(optional: Øystein Haugen, Knut Eilif Husa, Ragnhild Kobro Runde, Ketil Stølen: Why Timed Sequence Diagrams Require Three-Event Semantics. Scenarios: Models, Transformations and Tools 2003: 1-25) [pdf]

3. Live Sequence Charts

Date:

Student:

Supervisor:

Literature:

Werner Damm, David Harel: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design 19(1): 45-80 (2001) [pdf]
Yves Bontemps, Pierre-Yves Schobbens: The Complexity of Live Sequence Charts. FoSSaCS 2005: 364-378 [pdf]

4. Synthesis of state machines from Live Sequence Charts

Date:

Student:

Supervisor:

Literature:

Yves Bontemps, Patrick Heymans, Pierre-Yves Schobbens: From Live Sequence Charts to State Machines and Back: A Guided Tour. IEEE Trans. Software Eng. 31(12): 999-1014 (2005) [pdf]

5. Theory of regular languages of Message Sequence Charts

Date:

Student:

Supervisor:

Literature:

Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, Milind A. Sohoni, P. S. Thiagarajan: A theory of regular MSC languages. Inf. Comput. 202(1): 1-38 (2005) [pdf]

6. Semantics of sequence diagrams

Date:

Student:

Supervisor:

Literature:

David Harel, Shahar Maoz: Assert and negate revisited: modal semantics for UML sequence diagrams. SCESM 2006: 13-20 [pdf]
Radu Grosu, Scott A. Smolka: Safety-Liveness Semantics for UML 2.0 Sequence Diagrams. ACSD 2005: 6-14 [pdf]

7. Synthesis of distributed automata from MSCs

Date:

Student:

Supervisor:

Literature:

Madhavan Mukund, K. Narayan Kumar, Milind A. Sohoni: Synthesizing Distributed Finite-State Systems from MSCs. CONCUR 2000: 521-535 [pdf]

8. UML Statechart semantics

Date:

Student:

Supervisor:

Literature:

Michael von der Beeck: A structured operational semantics for UML-statecharts. SoSym 130-141, 2002 [pdf]
Stefania Gnesi, Diego Latella, Mieke Massink: Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking. J. Log. Algebr. Program. 51(1): 43-75 (2002) [pdf]

9. Stateflow semantics

Date:

Student:

Supervisor:

Literature:

Grégoire Hamon, John M. Rushby: An Operational Semantics for Stateflow. FASE 2004: 229-243 [pdf]
Grégoire Hamon: A denotational semantics for stateflow. EMSOFT 2005: 164-172 [pdf]

10. Model checking hierarchical state machines

Date:

Student:

Supervisor:

Literature:

Rajeev Alur, Mihalis Yannakakis: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3): 273-303 (2001) [pdf]

11. Timed UML state machines

Date:

Student:

Supervisor:

Literature:

Alexander Knapp, Stephan Merz, Christopher Rauh: Model Checking - Timed UML State Machines and Collaborations. FTRTFT 2002: 395-414 [pdf]

12 .Probabilistic and stochastic UML Statecharts

Date:

Student:

Supervisor:

Literature:

David N. Jansen, Holger Hermanns, Joost-Pieter Katoen: A QoS-Oriented Extension of UML Statecharts. UML 2003: 76-91 [pdf]
David N. Jansen, Holger Hermanns, Joost-Pieter Katoen: A Probabilistic Extension of UML Statecharts. FTRTFT 2002: 355-374 [pdf]

13. The Object Constraint Language (OCL): Semantics and extensions

Date:

Student:

Supervisor:

Literature:

Paul Ziemann, Martin Gogolla: OCL Extended with Temporal Logic. Ershov Memorial Conference 2003: 351-357 (auch: Technischer Bericht 1/03, Uni Bremen) [pdf]
Mark Richters, Martin Gogolla: OCL: Syntax, Semantics, and Tools. Object Modeling with the OCL 2002, LNCS 2263: 42-68 [pdf]

14. Liveness in sequence diagrams and the OCL

Date:

Student:

Supervisor:

Literature:

Alessandra Cavarra, Juliana Küster Filipe: Combining Sequence Diagrams and OCL for Liveness. Electr. Notes Theor. Comput. Sci. 115: 19-38 (2005) [pdf]
Alessandra Cavarra, Juliana Küster Filipe: Formalizing Liveness-Enriched Sequence Diagrams Using ASMs. Abstract State Machines 2004: 62-77 [pdf]

15. Timed extensions of the OCL

Date:

Student:

Supervisor:

Literature:

Juliana Küster Filipe, Stuart Anderson: On a time enriched OCL liveness template. STTT 8(2): 156-166 (2006) [pdf]
Stephan Flake, Wolfgang Müller: Past- and Future-Oriented Time-Bounded Temporal Properties with OCL. SEFM 2004: 154-163 [pdf]
Stephan Flake, Wolfgang Müller: An OCL Extension for Real-Time Constraints. Object Modeling with the OCL 2002: 150-171 [pdf]

16. Model checking UML activity diagrams

Date:

Student:

Supervisor:

Literature:

Rik Eshuis: Symbolic model checking of UML activity diagrams. ACM Trans. Softw. Eng. Methodol. 15(1): 1-38 (2006) [pdf]

BSc/MSc/Diploma Topics
Teaching WS 2012/13
Hybrid Systems Group

We are looking for a HiWi for the Compiler Construction course. If you are interested, please contact Thomas Noll.

Joost-Pieter Katoen has been appointed as a member of the renowned Academia Europaea (Academy of Europe), a European, non-governmental association acting as an Academy whose members are scientists and scholars who collectively aim to promote learning, education and research.

Vacancies for postdoctoral researchers in "Automated Analysis of Probabilistic Programs". Application deadline: August 15, 2013.

Joost-Pieter Katoen has been awarded a Distinguished Professorship from the RWTH Aachen University.

The Hybrid Systems: Computation and Control (HSCC'13) conference in Philadelphia has been very successful: Hongfei Fu received the best student paper award for his paper "Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata". Besides, the paper by Ilya Tkachev, Alexandru Mereacre, Alessandro Abate and Joost-Pieter Katoen was ranked second in the overall best paper award selection.

Joost-Pieter Katoen has been elected as Steering Committee Chair of ETAPS (www.etaps.org), the largest conference on theory and practice of software in Europe. He is the first non-UK ETAPS SC chair since the conference was initiated in 1998. More information here.

The Alumni-Magazine of RWTH Aachen University contains an interview with our former PhD student and postdoctoral researcher, Dr. Tingting Han.

HiWi's wanted to work in a new European Space Agency project for enhancing state-of-the-art design and analysis tools (COMPASS) for the next generation European rockets. Need programming and model checking affinity. See here for details and contact.

We offer openings for several PhD candidates in the area of
"Model-Based Design and Analysis for Dependable Software Systems". Deadline for application: September 14, 2012. For further information click here.

The Theory of Hybrid Systems Group offers two jobs as student assistants within the CEBug project. For more information, look here.

Dino Distefano received the prestigious Roger Needham Award for his work on software verification. This award is for a distinguished research contribution in computer science by a UK based researcher who has completed up to 10 years of post-doctoral research. Dr. Distefano was the first PhD student supervised by Joost-Pieter Katoen.

Marijn Jongerden received the German MMB (Messung, Modellierung und Bewertung von Rechensystemen) Award 2012 of the GI/ITG-Committee for Measurement, Modelling and Evaluation of Computing Systems for his PhD-thesis on "Model-based energy analysis of battery powered systems". His work was supervised by Boudewijn Haverkort (Twente) and Joost-Pieter Katoen.

Our paper "Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite" has been accepted to ICSE 2012 in the track SE in Practice (18% acceptance rate). The paper treats a new satellite from the European Space Agency that was modeled and analyzed with modern tools during the actual satellite design.

Joost-Pieter Katoen will act as DJ in the "Nacht der Professoren" in the Apollo bar and cinema.