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

  • Yves Bontemps

Thèse de l'étudiant: Master typesMaster en sciences informatiques

Résumé

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
la date de réponse2001
langue originaleAnglais
SuperviseurPIERRE-YVES SCHOBBENS (Promoteur) & Patrick HEYMANS (Promoteur)

Contient cette citation

'