Research area: Automata and Model-Checking

Of particular interest are techniques for the automated generation of test-cases from behavioral models — be it from process-algebras, from (extended) transition systems, LTL-like logics or descriptions in form of State-exception-Monads. In particular when combined with substantial data, behavioral models suffer in particular way from state-space explosion similarly to model-checking techniques. One possible anwer to the challenge is to use symbolic representations of models, their normal forms, symbolic states, the resulting test-cases (partitions of test-data) and constraint-solving techniques for test-data selection.


Aims and Scope:

The primary goal is finding compact, symbolic representations of automata, process-expressions and monadic representations of behaviour, that lend themselves to specifications combining data and behaviour. On this basis, procedures were investigated that explore symbolically traces and represent potentially infinite data-spaces by logical constraint systems. Of particular interest are combined methods and their tool implementations that allow for testing realistic applications, such as web-services and service integrations.


The HOL-TestGen/Cirta system (see activity Testing based on Process Algebra Specifications).

The Cubicle System  allowing for a semi-symbolic exploration of concurrent algorithms and protocols. 

The Monad Library as part of the HOL-TestGen HOL-TestGen System.



  • Marie-Claude Gaudel
  • Fatiha Zaidi
  • Delphine Longuet
  • Abdou Feliachi
  • Burkhart Wolff



Related Projects: 

Activities in this research area in more detail:  

You are here Research Automata and Model-Checking