### Abstracts

#### PATRICIA BOUYER

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. Bibliography: * R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science 126:183-235, 1994. http://www.cis.upenn.edu/~alur/Icalp90.ps.gz * 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 http://www.cis.upenn.edu/~alur/SFM04.ps * E. Asarin. Challenges in timed languages: From applied theory to basic theory. The Bulletin of the European Association for Theoretical Computer Science 83, 2004. http://www.cs.aau.dk/~luca/BEATCS/timedchall.pdf Tutorial in pdf-format available here.

#### 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. References 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

Please see this page.

#### Pierre Alain Muller

Applications of model transformations Slides in pdf-format available here.

#### REIKO HECKEL

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 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. Slides in pdf-format available here.

#### THIERRY JERON

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. http://www.springerlink.com/index/10.1007/s10009-004-0153-x [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. http://www.irisa.fr/vertecs/Publis/Ps/tacas05.pdf

#### 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-deter- ministic behaviour. Background material: basics on stochastic processes, e.g. lectures 10, 11, 12, 17 and 18 at http://www-i2.informatik.rwth-aachen.de/Teaching/Course/PMC/2005/PMC2005.html 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 http://fmt.cs.utwente.nl/publications/files/399_116221.pdf) Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen: On the Logical Characterisation of Performability Properties. ICALP 2000: 780-792 (see http://fmt.cs.utwente.nl/publications/files/33_bhhk.ps) Christel Baier, Marta Z. Kwiatkowska: Model Checking for a Probabilistic Branching Time Logic with Fairness. Distributed Computing 11(3): 125-155 (1998) (see http://www.cs.bham.ac.uk/~dxp/papers/distcomp98.ps.gz) Hans Hansson, Bengt Jonsson: A Logic for Reasoning about Time and Reliability. Formal Asp. Comput. 6(5): 512-535 (1994) (see ftp.sics.se/pub/SICS-reports/Reports/SICS-R--90-13--SE.ps.Z)

#### 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 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 controller. Readings: @inproceedings {asetooldemo04, author = "Mikucionis, Marius and Larsen, Kim G. and Nielsen, Brian", title = "T-Uppaal: Online Model-based Testing of Real-time Systems", booktitle = {19th IEEE International Conference on Automated Software Engineering}, year = 2004, month = september, note = "2~pp", url={http://www.cs.auc.dk/~bnielsen/Published/asetooldemo.ps} } @INPROCEEDINGS{fates04, 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}, ORGANIZATION = {}, YEAR = 2004, PUBLISHER = {}, PAGES = {}, ADDRESS = {Co-located with IEEE Conference on Automates Software Engineering 2004, Linz, Austria.}, MONTH = {September}, DATE = {21}, NOTE = {}, SERIES = {}, URL = {http://www.cs.aau.dk/~bnielsen/Published/fates04.ps} } @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 = "", url={http://www.cs.auc.dk/~bnielsen/Published/emsoft05.ps} }

#### ILEANA OBER

Please see this page.

#### JEAN FRANCOIS RASKIN

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 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. Abstract: 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. http://www-verimag.imag.fr/~tripakis/papers/tadiag.pdf Other references available at: http://www-verimag.imag.fr/~tripakis/testing.html

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

Title: Foundations of Testing Slides in pdf format available here.