ARTIST2 Summer School on Component & Modelling, Testing & Verification, and Statical Analysis of Embedded Systems, Sept 29 - Oct 2, 2005
home | programme | venue & travel | registration | steering committee | local organisers | invitation | photos



TUTORIAL: Foundation for Timed Systems
Patricia Bouyer, ENS Cachan, France

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. 


* R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer 
  Science 126:183-235, 1994.
* 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
* E. Asarin. Challenges in timed languages: From applied theory to basic 
  theory. The Bulletin of the European Association for Theoretical Computer 
  Science 83, 2004.

Tutorial in pdf-format available here.


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


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

Compositional Modeling in Metropolis, Gregor Goessler and Alberto
Sangiovanni-Vincentelli, Proc. EMSOFT'02, A. Sangiovanni-Vincentelli and
J. Sifakis, October, 2002


Please see this page.

Pierre Alain Muller

Applications of model transformations

Slides in pdf-format available here.


Foundations of Model Transformations

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

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.

Slides in pdf-format available here.


Test Generation using Model Checking
Thierry Jéron, Irisa/Inria Rennes, France
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.

 [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.

 [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.


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-deter-
ministic behaviour.

Background material: 
basics on stochastic processes, e.g. lectures 10, 11, 12, 17 and 18 at

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)

Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: 
On the Logical Characterisation of Performability Properties. ICALP 2000: 

Christel Baier, Marta Z. Kwiatkowska: Model Checking for a Probabilistic 
Branching Time Logic with Fairness. Distributed Computing 11(3): 125-155 
(1998) (see

Hans Hansson, Bengt Jonsson: A Logic for Reasoning about Time and Reliability. 
Formal Asp. Comput. 6(5): 512-535 (1994)


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 relativized
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


@inproceedings {asetooldemo04,
   author =	 "Mikucionis, Marius and Larsen, Kim G. and Nielsen,
   title =	 "T-Uppaal: Online Model-based Testing of Real-time Systems",
booktitle = {19th IEEE International Conference on Automated Software 
   year =	 2004,
   month =	 september,
   note =	 "2~pp",

   AUTHOR = {Kim Larsen and Marius Mikucionis and Brian Nielsen},
   TITLE = {{Online Testing of Real-time Systems using Uppaal}},
   BOOKTITLE = {International workshop on Formal Approaches to Testing 
of Software},
   YEAR = 2004,
   PUBLISHER = {},
   PAGES = {},
   ADDRESS = {Co-located with IEEE Conference on Automates Software 
Engineering 2004, Linz, Austria.},
   MONTH = {September},
   DATE = {21},
   NOTE = {},
   SERIES = {},
   URL = {}

@inproceedings {emsoft05,
   author =	 "Mikucionis, Marius and Larsen, Kim G. and Nielsen,
                   Brian and Skou, Arne",
   title =	 "Testing Real-Time Embedded Software using UppAal-TRON ---an 
industrial case study",
booktitle = {Embedded Software (EMSOFT)},
   year =	 2005,
   month =	 september,
   note =	 "",


Please see this page.


Title : Timed Controller Synthesis and Implementability Issues

Slides in pdf-format available here.

Abstract : 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  

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.


Please see this pdf document.


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.

Other references available at:


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.


Title: Foundations of Testing

Slides in pdf format available here.