Abstract
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 Award | 2001 |
|---|---|
| Original language | English |
| Supervisor | Pierre Yves Schobbens (Supervisor) & Patrick Heymans (Supervisor) |