Module "Verification and Testing of Embedded Systems" (VTS)
Head: Sophie Pinchinat
Keywords: operational models, timed systems, automata,
logics, infinite games, component-based systems, interface,
verification, testing, control-flow graph, coverage, oracle.
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 methodologies rely on formal modelling (capturing
the relevant features of the system and its desirable properties)
followed by algorithmic analysis. 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 in the
environment is naturally modelled by probabilistic state changes.
Testing, while being the most used validation technique to assess the
quality of embedded systems, often remains an ad hoc process. But
despite its experimental nature, testing can be formal too, relying on
models of software artefacts and well-founded theories, and can then be
(partly) automated using algorithmic analysis and synthesis (based on
symbolic execution, constraint solving and verification techniques).
This is encompassed by the term model-based testing of the literature.
The first part of the course provides the students with fundamental
notions in formal modelling and related algorithmic analysis, while
developing their skill to use/design appropriate formalisms, and their
discernment to evaluate whether these formal frameworks are amenable to
effective methods.
The second part of the course focuses on testing, more precisely on
automated test selection, from code models (white-box, structural
testing) and from specification models (black box, conformance
testing). The goal is to show that formalization can seriously improve
testing automation.
Lectures and material on Structural Testing (6h)
Lectures and material on Conformance Testing (4h)
Material Lecture1, Lecture2
Bibliography
- J. Tretmans. Test Generation with Inputs, Outputs and Repetitive Quiescence , Software-Concepts and Tools, 17(3), pp 103-120, 1996
- 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), 6, October 2004.
- M. Broy, B. Jonsson, J.-P. Katoen, M. Leucker, A. Pretschner (eds.), Model-Based Testing of Reactive Systems. LNCS 3472, Springer Verlag, 2005.
Lectures and material on Timed Automata (4h)
Lectures and material on Automata, Logics and Infinite Games (6h)