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 group develops methods and tools for following different approaches to system validation and verification:

altrandom-based model exploration automata and model-cheking proof techniques and logical representations Security Infrastructures Embeded Systems C Code Web Services Service Integration
  • proof-based black-box testing from logical representations,
  • active and passive testing from behavioural models,
  • white-box testing using random exploration methods.

Random methods are also used for model-checking purposes.

The work 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 distributed and communicating systems (communication protocols, Web services), critical embedded systems (transportation applications) and security infrastructures.

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.
  • Auguste++ is a white-box statistical testing tool for C programs.
  • Rukia is a C++ library for model exploration by uniform random walk.
  • The group also makes major contributions to Isabelle/HOL as a platform for the development of correct Formal Methods Tools.
You are here Home