Computer systems play a central role in modern societies and their
errors can have dramatic consequences. Industry and academics thus
invest a considerable amount of effort developing techniques to prove
the correctness of these systems. Among such techniques, one finds (1)
testing, the traditional approach to detect bugs with test
cases, and (2) formal methods, e.g., model checking (Turing
award), that can guarantee the absence of bugs.
Both approaches have been largely deployed on static systems, whose
behaviour is entirely known. ESTASYS focuses on developping
brand new formal methods for Systems of Systems.
Statistical Model Checking
International and industrial relations
Université de Namur
University of Trento
University of Copenhagen
Université de Vannes
University of Dortmund
University of Vienna
Royal Holloway University of London
ESTASYS is an exploratory action and Inria team that proposes inovative techniques for the rigorous design of Cyber Physical Systems (CPS). ESTASYS focuses on :
- New efficient simulation techniques used to overcome both the undecidability and state-space explosion problems
- New quantitative techniques to reason on complex properties such as resource allocation and energy budget.
- New techniques to quantify privacy and information flow (secure passwords, etc)
- New revolutiony tools and integrated libraries.
- New contract theories for requirement specifications.