ARTIST2 Summer School 2005

September 29th - October 2nd 2005       Nässlingen, Sweden organised and funded by ARTIST 

Abstracts and Slides

Be sure to see the school’s overview.

 

Contents - Abstracts and Slides for the following speakers:
- Patricia Bouyer
- Alberto Ferrari
- Susanne Graf
- Pierre Alain Muller
- Reiko Heckel
- Thierry Jeron
- Joost-Pieter Katoen
- Brian Nielsen
- Ileana Ober
- Jean François Raskin
- Joseph Sifakis
- Stavros Tripakis
- Reinhard Wilhelm
- Ed Brinksma


Patricia Bouyer

Tutorial: Foundation for Timed Systems

- Slides in pdf-format available here.

Many critical applications have explicit timing constraints. For example, behaviours of systems interacting with an environment (e.g. embedded systems) depend on quantitative timing constraints like response times, transmission delays, etc... For representing such timed systems, several timed models have been proposed. Since their introduction by Alur and Dill in the 90s, timed automata are one of the most-studied and most-established models for real-time systems. Numerous works have been devoted to the comprehension of timed automata and the major property of timed automata is probably that reachability is decidable, which implies in particular that it can be used for verification purposes. Based on this nice theoretical result, several model-checkers have been developed (for instance CMC, HyTech, Kronos and Uppaal) and a lot of case studies have been treated.
In this tutorial, we will present the model of timed automata, and basic but fundamental results on this model.

Bibliography:
  • R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science 126:183-235, 1994.
    See it online!
  • R. Alur and P. Madhusudan. Decision problems for timed automata: A survey. 4th Intl. School on Formal Methods for Computer, Communication, and Software Systems: Real Time, 2004.
    See it online!
  • E. Asarin. Challenges in timed languages: From applied theory to basic theory. The Bulletin of the European Association for Theoretical Computer Science 83, 2004.
    See it online!


Alberto Ferrari

Modeling of Heterogeneous Systems in Metropolis

Establishing formal design methodologies is imperative to effectively manage complex design tasks required in modern-date system designs. It involves defining levels of abstraction to represent formally systems being designed, as well as formulating problems to be addressed at and across the abstraction levels. This approach calls for a design environment in which systems can be unambiguously represented throughout the abstraction levels, the design problems can be mathematically formulated, and tools can be incorporated to solve some of the problems automatically. Developing such an environment is precisely the goal of Metropolis. Metropolis consists of an infrastructure, a tool set, and design methodologies for various application domains. Metropolis is based on the concept of metamodel, as a way of capturing in a semantic rigorous way the interconnection of subsystems described with different models of computation. By the same metamodeling approach, we can integrate and apply tools for formal methods easily. In addition, the Metropolis infrastructure allows decorating functional models of the design with non functional properties such as execution time and power consumed. Because of its flexibility and expressive power, the framework can be used in a variety of industrial domains.

In this talk, I will review the architecture of the environment, its semantics, models of computation supported, and the application of the Platform-based Design methodology via Metropolis to a number of case studies.

Bibliography:
  • Metropolis Design Guidelines, Alessandro Pinto, University of California at Berkeley, UCB/ERL Memo 04/40, November, 2004.
  • The Metropolis Meta Model Version 0.4, The Metropolis Project Team, University of California, Berkeley, UCB/ERL M04/38, September, 2004.
  • Simple Case Study in Metropolis, Abhijit Davare, Douglas Densmore, Vishal Shah, Haibo Zeng, University of California, Berkeley, UCB.ERL 04/37, September, 2004.
  • Microarchitecture Development via Metropolis Successive Platform Refinement, Douglas Densmore, Sanjay Rekhi, Alberto Sangiovanni-Vincentelli, Design Automation and Test in Europe (DATE), February, 2004.
  • Separation of Concerns: Overhead in Modeling and Efficient Simulation Techniques, G Yang, Y Watanabe, F Balarin, A Sangiovanni-Vincentelli, Fourth ACM International Conference on Embedded Software (EMSOFT’04), September, 2004.
  • Metropolis: An Integrated Electronic System Design Environment, Felice Balarin, Yosinori Watanabe, Harry Hsieh, Luciano Lavagno, Claudio Passerone, Alberto Sangiovanni-Vincentelli, IEEE Computer Society, April 2003.
  • Compositional Modeling in Metropolis, Gregor Goessler and Alberto Sangiovanni-Vincentelli, Proc. EMSOFT’02, A. Sangiovanni-Vincentelli and J. Sifakis, October, 2002.


Susanne Graf

Verification of UML models with timing constraints with IF

- Slides in pdf format are available here.

This talk will give an overview on the IF, an open validation platform for asynchronous timed systems such as telecommunication protocols or distributed embedded applications. The IF toolbox is built upon a specification language based on timed automata with urgency extended with discrete data variables, various communication primitives, dynamic process creation and destruction. This language includes most of the concepts allowing the direct representation of modeling and programming languages for distributed systems like SDL, UML or Java, as well as extensions allowing the expressions of timing properties.
Here, we will focus on the use of IF for the validation of real-time properties of UML models. A short overview on the considered UML profile and the mapping principles from UML to IF will be presented, as well as the way in which semantic variations of the profile are anticipated. Then the usefulness of the UML profile for modelling of real-time systems and their properties, and the use of the IF toolset for their validation will be demonstrated on hand of one or two case studies. In particular, we will show the use of the considered UML profile for the validation of deployment related propserties such as scheduling and timely access to a shered bus.
This talk is related to the talk on Component-based modeling of real-time systems (see the program ). Several of the concepts presented in this talk have been implemented in IF and have shown their usefulness for obtaining faithful and direct mappings of high-level modeling languages.

A list of related documents and links :
  • The webpage of the IF verification platform containing links to manuals, downloadable code, case studies and contains also a tutorial.
  • Below a few papers on the IF language and tool and the theory behind:
    o The paper presented at CAV 2002 explains the difference to the older versions of the language and the tool
    o The paper presented at SFM summer school 2004 gives a complete overview on the IF language and the tool architecture.
    o This paper which has been published in Information and Computation introduces timed automata with urgency which are the version of timed automata used in IF
    o This paper which has been presented at the Symposium FMCO 2003 shows the expressive power of priorities. Indeed, priorities have been very helpful for the mapping of different high level formalisms to IF.
  • The webpage of the Omega project in which the considered UML profile and the UML interface IFx for IF have been developed.
  • Below a few papers on the UML profile, in particular the real-time extensions and the work in connection with the IF tool. Overviews on all work done in Omega can be found on the Omega home page.
    o This paper which is being published in STTT gives an overview on the mapping from UML to IF, the IFx frontend and one of the case studies
    o This paper which is being published in STTT explains in details the real-time extensions of the UML profile.
    o This paper presents a case study carried out in the context of the Omega project and is to be presented at the MARTES workshop. Another case study is in this paper, and the Omega web page gives an overview on all case studies


Pierre Alain Muller

Applications of model transformations

- Slides in pdf-format available here.


Reiko Heckel

Foundations of Model Transformations

- Slides in pdf-format are available here.

At the heart of model-driven engineering are activities like maintaining consistency, evolution, translation, and execution of models. These are examples of model transformations. A (mathematical) foundation is needed for studying issues like the expressiveness and complexity, execution and optimisation, well-definedness and semantic correctness of transformations. This lecture is about graph transformations as one such foundation.
After introducing the basic concepts of graph transformation by means of an example, different applications of graph transformations to model transformations will be discussed. A survey of relevant theory and tools concludes the presentation.


Thierry Jeron

Test Generation using Model Checking

In this talk, we will show how verification techniques (model-checking, abstract interpretation) can be used for the automatic generation of test cases for conformance testing of reactive systems. Conformance testing consists in checking, using test cases, whether a black box implementation behaves correctly with respect to a formal specification.
In the ioco testing theory [Tretmans96], the operational semantics of a (non-deterministic) system (specification, implementation or test case) is modelled by a transition system with inputs and outputs (IOLTS) and conformance is defined as a relation between visible behaviors of the implementation and the specification.
A crucial problem in this context is to select off-line some test cases from the specification, before executing them on the implementation. One possible solution is to use test purposes specified by observers accepting behaviors one wants to observe during testing. Test case selection then mainly reduces to a language intersection problem (computing a subset of the visible behaviors of the specification accepted by a test purpose), which amounts to solving reachability and co-reachability problems in a product model.
For finite state systems, these problems can be solved by classical graph algorithms, as implemented in the TGV tool [Jard-Jeron]. For more powerful specification models like extended automata (IOSTS), one wants to select test cases in the form of extended automata, by syntactic operations. But because reachability and co-reachability problems are undecidable in these models, over-approximations (e.g. computed by abstract interpretation) can be used to guide the syntactic transformations [Jeannet et al.05]. These algorithms are implemented in the STG tool.

Bibliography:
  • [Tretmans96] J. Tretmans. Test Generation with Inputs, Outputs and Repetitive Quiescence. Software - Concepts and Tools, Vol. 17(3), pp. 103 - 120. Springer-Verlag, 1996.
    Also: Technical Report No. 96-26, Centre for Telematics and Information Technology, University of Twente, The Netherlands.
  • [Jard-Jeron 04] C. Jard, T. Jéron. TGV: theory, principles and algorithms, A tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems, Software Tools for Technology Transfer (STTT), Volume 7, No 4, August 2005.
    See it online!
  • [Jeannet et al.] B. Jeannet, T. Jéron, V. Rusu, E. Zinovieva. Symbolic Test Selection based on Approximate Analysis, in TACAS’05, Volume 3440 of LNCS, Edinburgh (Scottland), April 2005.
    See it online!


Joost-Pieter Katoen

Model checking focuses on absolute correctness ("either the system is safe or not"). In practice such rigid notions are hard, or even impossible, to guarantee. Instead, systems are subject to various phenomena of stochastic nature, such as message loss, faults, and delays. Correctness thus has a less absolute nature. Quantitative properties ("safety is guaranteed in 93% of the cases") can be automatically checked using stochastic model checking.
This technique originates from the mid 1980s focusing on establishing 0-1 probabilities ("a program terminates with probability one"). During the last decade, these methods have been extended, refined and improved, and - most importantly - are nowadays supported by software tools that have been applied to analyze real-life systems e.g., Bluetooth’s device discovery, IPv4 address assignment, and group membership protocols for wireless networks.
This tutorial will survey the foundations of model checking of stochastic process of different nature, such as discrete-time, continuous-time, cost- extended models as well as models exhibiting probabilistic and non-deterministic behaviour.

Background material:
  • Basics on stochastic processes, e.g. lectures 10, 11, 12, 17 and 18.
    See it online!

Fundamental papers on this topic
  • Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng. 29(6): 524-541 (2003).
    See it online!
  • Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: On the Logical Characterisation of Performability Properties. ICALP 2000: 780-792.
    See it online!
  • Christel Baier, Marta Z. Kwiatkowska: Model Checking for a Probabilistic Branching Time Logic with Fairness. Distributed Computing 11(3): 125-155 (1998).
    See it online!
  • Hans Hansson, Bengt Jonsson: A Logic for Reasoning about Time and Reliability. Formal Asp. Comput. 6(5): 512-535 (1994).
    See it online!


Brian Nielsen

Automated model-based testing of real-time systems poses a new set of challenges: It must be defined when a system is correct with respect to real-time requirements. The test selection problem is worsened because in real-time systems there are an infinite set of time instances to choose from about when to supply inputs expect outputs. The test cases or formal model must be interpreted in real-time requiring new symbolic analysis algorithms. Finally tests must be executed and the implementation monitoring in real-time.
In this tutorial we present a framework, an algorithm and a new tool for online testing of embedded real-time systems based on symbolic techniques used in \uppaal model checker engine. Using online testing, tests are generated and immediately executed event per event. We describe a sound and complete randomized online testing algorithm and how to implement it using symbolic state representation and manipulation techniques. We propose the notion of relatvized timed input/output conformance as the formal implementation relation. A novelty of this relation and our testing algorithm is that they explicitly take environment assumptions into account, generate, execute and verify the result online. Finally, we show how the framework and tool can be applied to an industrial embedded controller.

Bibliography
  • Mikucionis, Marius and Larsen, Kim G. and Nielsen,Brian. T-Uppaal: Online Model-based Testing of Real-time Systems, 19th IEEE International Conference on Automated Software Engineering, 2004, september, 2 pp.
    See it online!
  • Kim Larsen and Marius Mikucionis and Brian Nielsen, Online Testing of Real-time Systems using Uppaal, International workshop on Formal Approaches to Testing of Software, 2004, Co-located with IEEE Conference on Automates Software Engineering 2004, Linz, Austria, September 21.
    See it online!
  • Mikucionis, Marius and Larsen, Kim G. and Nielsen, Brian and Skou, Arne, Testing Real-Time Embedded Software using UppAal-TRON --- an industrial case study, Embedded Software (EMSOFT), September 2005.
    See it online!


Ilena Ober

- Slides are available here.

UML (Unified Modeling Language) is a standardised (set of) language(s) allowing to specify, design, visualize and document models of software systems. UML does not impose a development process or methodology and it aims at being independent of any programming language.
In UML, the user can specify requirements, model the system’s logical structure and behaviour (as a whole or by decomposition into subsystems and components), describe physical deployment and platform-specific information, annotate and document the model. By covering various facets of software development at various points of its lifetime, UML provides a concrete support for model driven development.
This tutorial presents the major features of UML, with focus on system and components modelling of structure and behaviour.

Resources and links - UML Standard Specifications
UML is a subject of frantic writing. There are lots of books describing UML, giving different interpretations for it, suggesting how to use it in various contexts, how to adapt it for fitting various needs… Therefore, to me, The most important references are the (user unfriendly) documents composing the OMG standard.
You can always find the most up-to-date standard UML specifications here.

The reference specifications for UML 2.0 (august 2005) are:

Those still interested in UML 1.x can find the specification for UML 1.4.2 (the UML specification also standardised by ISO) here.

A little known, yet quite interesting OMG working document containing an assessment on the use of UML 1.x performed before starting the work on UML 2.0.

UML biographies

Other ressources
An overview of (some) UML-based tools can be found here.

"Classical" UML critiques:
  • Death by UML fever, by Alex E. Bell, on the occasional misuse of UML
  • Bertrand Meyer’s 1997 satire on UML published in a special issue of Ed Yourdon’s American Programmer UML: The Positive Spin


Jean François Raskin

- Timed Controller Synthesis and Implementability Issues

- Slides in pdf-format available here.

In this talk, I will show how to formalize the controller synthesis problem using two-player games. First, I will consider reachability and safety games on finite game structures. Second, I will consider those games on (infinite) timed game structures and show how to synthesize strategies that have desirable properties like non-zenoness. Third, I will show that some non-zeno strategies are not implementable and I will introduce the notion of Almost ASAP semantics which allow to solve the implementability problem for timed automata.

Two papers to read :
  • Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar,
    Mariëlle Stoelinga. The element of surprise in timed games. In the
    Proc. of CONCUR’03, LNCS , Springer-Verlag, p. 142-156, 2003.
  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Almost ASAP
    Semantics: From Timed Models to Timed Implementations. In the Proc.
    of HSCC’04, LNCS 2993, Springer-Verlag, p. 296-310, 2004.
  • More pointers to relevant papers will be given during the talk.


Joseph Sifakis

- Please see this pdf document.


Stavros Tripakis

- A more recent abstract is available in this pdf document.

We study the problem of fault-diagnosis in the context of dense-time automata. The problem is, given the model of a plant as a timed automaton with a set of observable events and a set of unobservable events, including a special event modeling faults, to construct a deterministic machine, the diagnoser, which reacts to observable events and time delays, and announces a fault within a delay of at most Delta time units after the fault occurred. We define what it means for a timed automaton to be diagnosable, and provide algorithms to check diagnosability. The algorithms are based on standard reachability analyses in search of accepting states or non-zeno runs. We also show how to construct a diagnoser for a diagnosable timed automaton, and how the diagnoser can be implemented using data structures and algorithms similar to those used in most timed-automata verification tools.

Main reference:
  • S. Tripakis. Fault Diagnosis for Timed Automata. In FTRTFT’02. LNCS 2469, Springer.
    See it online!
  • Other references available here.


Reinhard Wilhelm

Timing Analysis for Real-Time Systems

Hard real-time systems are subject to stringent timing constraints which are dictated by the surrounding physical environment. A schedulability analysis has to be performed in order to guarantee that all timing constraints will be met ("timing validation"). Existing techniques for schedulability analysis require upper bounds for the execution times of all the system’s tasks to be known. These upper bounds are commonly called worst-case execution times (WCETs).
The WCET-determination problem has become non-trivial due to the advent of processor features such as caches, pipelines, and all kinds of speculation, which make the execution time of an individual instruction locally unpredictable. Such execution times may vary between a few cycles and several hundred cycles.

A combination of Abstract Interpretation (AI) with Integer Linear Programming (ILP) has been successfully used to determine precise upper bounds on the execution times of real-time programs. The task solved by abstract interpretation is to compute invariants about the processor’s execution states at all program points. These invariants describe the contents of caches, of the pipeline, of prediction units etc. They allow to verify local safety properties, safety properties who correspond to the absence of "timing accidents". Timing accidents, e.g. cache misses, pipeline stalls are reasons for the increase of the execution time of an individual instruction in an execution state.


Ed Brinksma

Foundations of Testing

- Slides in pdf format available here.
- StatCounter - Free Web Tracker and Counter

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet