Quasimodo Workshop at Formal Methods 2009

---

Coping with Complexity and Quantitative Constraints

in Embedded Systems Design.

The design of embedded system is becoming increasingly complex and difficult due to the size and number of features they support. Moreover, they must satisfy a multitude of quantitative constraints including the resources that a system may use (computation resources, power consumption, memory usage, communication bandwidth, costs, etc.), assumptions about the environment in which it operates (arrival rates, hybrid behaviour), and requirements on the services that the system has to provide (timing constraints, QoS, availability, fault tolerance, etc.). These challenges call for advanced model-based development techniques and tools to support their design and implementation, including all development activities ranging from specification, analysis, design, code- and controller synthesis and testing. Quasimodo (www.quasimodo.aau.dk)  is a European research project under FP7 whose objective is to develop theory and techniques for handling quantitative constraints in the model-driven development of real-time embedded systems.

The purpose of this workshop arranged by Quasimodo is to bring researchers, practitioners and industry together to discuss the issues, challenges and latest solutions for the design of complex embedded systems with quantitative constraints. The workshop is especially targeted towards practitiones in the field but is open to everybody interested.

The workshop will feature a number of distinguished presentations on industrial challenges, new techniques offered by academia, case studies, and tool demonstrations.

Registration will be handled through the FMWeek registration system.

Programme NB UPDATED

9.00 - 10.00 Session 1: Keynote

  • Formal Methods, from Practice to Theory
    Rance Cleaveland, University of Maryland
10.30-10.45 Introduction to Quasimodo

  • Brief introduction to the project.
    Brian Nielsen, Aalborg University, Denmark
10.45-12.15 Session 3: Model-based Controller Synthesis and Scheduling analysis

  • Terma Case: Schedulability Analysis using Uppaal,
    Aalborg University, Denmark
  • Introduction to the Hydac Hydraulic Pump Control Case,
    Kai Mittelmüller, Hydac Gmbh
  • Automated Controller Synthesis with the Uppaal-Tiga tool chain,
    Jean Francois Raskin, Université Libre de Bruxelles
13.30 - 15.30 Session 2: Model-based analysis of the Chess wireless sensor network case
  • Introduction to the Chess WSN case,
    Marcel Verhoef, Chess
  • Analysing Timing of the WSN MAC Protocol,
    Frits Vaandrager, University of Nijmegen
  • Model Based Testing for embedded systems,
    Jan Tretmans, Embedded Systems Institute, NL
  • Advances in Probabilistic Verification,
    Joost-Pieter Katoen, RWTH Aachen

15.30 - 16.00 Session 4: Panel discussion

Abstracts and further details will be announced at: http://www.quasimodo.aau.dk/qws/


Formal Methods, from Practice to Theory:

Rance Cleaveland

A common topic of discussion in the formal-methods community concerns the lack of uptake in industry of these techniques. Various explanations are typically offered, including lack of mathematical sophistication by possible users, problems of scaling formal methods "up" to industrial problems, lack of consistent instruction on the techniques within universities, and others. In this talk I will draw on my experience in starting a company to commercialize formal methods to suggest an alternative explanation for the state of affairs, and to propose alternative approaches to changing it.

Modelling Clock Synchronization in the Chess gMAC WSN Protocol

Frits Vaandrager, Faranak Heidarian, Julien Schmaltz, Marcel Verhoef

In this talk, we report on some synchronizations that took place between the Radboud University Nijmegen (RUN) and the Dutch Company Chess within the context of the EU project QUASIMODO. RUN constructed a detailed timed automata model of the clock synchronization algorithm that is currently being used in a wireless sensor network that has been developed by Chess. Using the Uppaal model checker, it was established that in certain cases a static, fully synchronized network may eventually become unsynchronized if the current algorithm is used, even in a setting with infinitesimal clock drifts. We discuss the difficulties of applying timed automata technology in an industrial setting, the relevance of the results that were obtained, and some challenges that still need to be addressed.

Advancements in Probabilistic Model Checking:

Joost-Pieter Katoen

Soon after the birth of the flourishing research area of model checking in the early eighties, researchers started to apply this technique to finite automata equipped with probabilities. The initial focus was on qualitative properties - e.g., does a program terminate with probability one? - but later efficient algorithms were developed for quantitative questions as well.
Model checking of probabilistic models received quite some attention in the late nineties, and this popularity lasts until today. Some application areas are security, randomised distributed algorithms, systems biology, and classical performance analysis.
What is the current state of this field? Probabilistic verification, quo vadis? This talks surveys the main achievements during the last years, in particular during the Quasimodo project, reports on some recent advances, and attempts to point out some research challenges.

Model-based Testing of Real-time systems:

Jan Tretmans and Julien Schmaltz

Systematic testing is important for system and software quality, but it is also error-prone, expensive, and time-consuming. Model-based testing is a new technology that can improve the effectiveness and efficiency of the testing process. With model-based testing a system under test is tested against a formal description, or model, of the system's behaviour. Such a model serves as a precise and complete specification of what the system should do, and, consequently, is a good basis for the automatic generation of test cases and the analysis of test results. Quasimodo has worked on extending the basic model-based testing theory for state-based models (labelled transition systems) towards testing of quantitative properties, such as realtime and unbounded data domains. This has resulted in theories, tools, and applications of realtime and data-aware model-based testing. In this presentation we explain the ideas and principles of model-based testing and their realtime and data-aware extensions. Moreover, we will discuss how model-based testing has been applied to the new electronic passport and to conformance testing of the Chess wireless sensor network node using the model-based testing tools TorXakis and Uppaal-TRON.