Formal Testing and System Exploration
The research of the ForTesSE group is dedicated to formal methods and their applications to soft- and hardware systems. Particular emphasis is put on combinations of Test and Proof techniques.
The fundamental research underlying our approaches to system validation and verification can be categorized as follows:
- model-based testing using logical representations and proof techniques,
- random-based exploration methods, and
- automata and model-checking for behavioural models.
The fundamental research of the group relies on theoretical activities around the formalisms used for specification and modelisation (logics, transition systems, process algebras) and their associated verification methods (theorem proving, symbolic evaluation) or exploration methods (random-based exploration of large models or programs).
The application domains of this work cover security infrastructures, critical embedded systems (operating systems, medical devices) as well as distributed and communicating systems (communication protocols, Web services). A further domain consists in the development of test-generation methods for "real" programming languages.
The group has developed several tools based on innovative technology, that have been experimented on several case studies:
- HOL-TestGen is a test case generator, built on top of Isabelle/HOL, for theorem-proving based unit and sequence testing.
- The group also makes major contributions to Isabelle/HOL as a modeling platform as well as implementation framework for Formal Methods Tools.
- Rukia is a C++ library for model exploration by uniform random walk.
- Auguste++ is a white-box statistical testing tool for C programs.