Module "Verification and Testing of Embedded Systems" (VTS)
Master Recherche Informatique 2011-2012
Head: Sophie Pinchinat
Teachers: Nathalie Bertrand, Thierry Jéron, Sophie Pinchinat
Pre-requisites: propositional logic, graph and automata
theories and algorithms, basic notions of computational complexity.
Synopsis
Computer-system design currently relies on complex assemblages of
interacting components, which communicate and share resources in order
to achieve services; their use in safety-critical situations calls for
systemic modelling, verification and testing methodologies to check
both functional requirements (the expected services, functionalities,
and features, independent of the implementation) and non-functional
requirements (performance like timing, power consumption, execution
constraint, memory use, size, weight, and robustness like fault
tolerance, accessibility of resources, resistance to failure or to
attack, etc.), knowing that the major sources of complexity are
concurrency, real time and uncertainty.
Formal verification methods rely on formal modelling (capturing the
relevant features of the system and its desirable properties) followed
by algorithmic analysis. For example, the cooperative / adversarial
interaction between concurrent components of a system (or the system
and its testing environment) can be modelled as a multi-players game.
The real-time feature requires models that combine discrete state
transitions and continuous state evolutions. Uncertainty on the
environment is naturally modelled by probabilistic state changes.
This course addresses some classic approaches and techniques in the
wide field of formal verification.
The first part of this course concerns
complex systems verification. We consider extensions of automata
to model systems with rich features. We present two classical types of
automata: timed automata, which allow for analyzing timing constraints,
and Markov decision processes, which describe systems evolving is a
partially specified environment. For both types, we study their
expressiveness and describe verification methods: reachability
analysis for timed automata, and the model-checking of a probabilistic logic for Markov decision processes. .
The second part of this course focuses
on the representation of functional properties. We examine
different alternatives to represent systems: either in logic (here, we
consider the propositional mu-calculus, which subsumes all temporal
logics used for verification), or tree automata (as acceptors of tree
languages). Tree automata accept (the tree unfolding) of models of
formulas. In this setting, (parity) games play a fundamental role: they
provide the semantics of tree automata and enable to derive useful
algorithms for automated verification.
The third part of the course is about
model-based conformance testing. After an introduction to
conformance testing, we study the testing theories and automatic test
generation from two kind of models. In a first part, we consider simple
models of transition systems with inputs/outputs, named IOLTS, the
underlying testing theory funded on the conformance relation
ioco, and test generation in this context. In the second part, we
consider timed models with inputs/outputs (TAIO), we study the
underlying testing theory funded on the conformance relation tioco, and
the more involved problems of test generation that follow.
Keywords: transition systems,
timed systems, Markov chains, Markov decision processes, tree automata,
temporal logic, propositional mu-calculus, parity games, model-based
testing.
Prerequisite: propositional logic, automata (and graph) theory and
algorithmics, (basic notions on) computability and complexity.
General structure and content:
• Timed automata (4h): region, reachability
analysis, bisimulation, undecidable problems
• (Probabilistic) Model-checking (4h)
• The trilogy « Automata, Logic and (infinite) Games»
(8h): tree automata, propositional mu-calculus, parity games
• Model-based conformance testing (4h)
Bibliography
- C. Baier and J.-P. Katoen. Principles
of Model-checking. MIT Press, 2009.
- Automata, logics, and infinite
games: A guide to current research. Eds : Grädel E., Thomas W.,
Wilke T., outcome of a Dagstuhl seminar, February 2001, Springer, ISBN
3-540-00388-6, 2002.
- J. Tretmans. Test generation
with inputs, outputs and repetitive quiescence. Software -
Concepts and Tools, 3:103-120, 1996.
- N. Bertrand, T. Jéron, A. Stainer, M. Krichen. Off-line Test Selection with Test Purposes
for Non-Deterministic Timed Automata. In 17th International
Conference on Tools and Algorithms for the Construction And Analysis of
Systems (TACAS), LNCS, Volume 6605, Pages 96-111, Saarbrücken,
Germany, April 2011.
Slides
Slides on Timed
Automata (by Nathalie Bertrand)
Slides on Probabilistic
Model-Checking (by Nathalie Bertrand)
Slides on Automata, Logic and Games (by Sophie Pinchinat) Slides, Slides4x4
Forthcoming slides on
Model-based Conformance Testing (by Thierry Jéron)
Schedule of the Master's courses
The full schedule can be found here.
Assessments (2)
A written exam in December 2011.