Automated verification of state-based specifications against scenarios: a step towards relating inter-object to intra-object specifications

  • Yves Bontemps

Student thesis: Master typesMaster in Computer science


While designing a system, it is critical to ensure that its behavioral specification is correct with respect to its requirements. These requirements are often described as a set of scenarios instantiating use-cases. Formai and automated verification of this correctness is desirable in this context. To formally describe scenarios, we use LSCs [Harel 98a], an extension of Message Sequence Charts (MSCs) allowing the expression of both safety and liveness conditions. An algorithm to automatically translate LSCs into temporal logic is presented. The obtained formulae can then be used by a model-checker to prove the correctness of the specification. Hence, a total automation of the verification process is obtained.
To achieve a better efficiency in verification, we then refine the translation, by splitting the formula into several smaller formulae. Again, we exhibit an algorithmic solution to support these methods
Date of Award2001
Original languageEnglish
SupervisorPIERRE-YVES SCHOBBENS (Supervisor) & Patrick HEYMANS (Supervisor)

Cite this