Tool-Assisted Multi-Facet Analysis of Formal Specifications (Using Alelier-B and ProB)

J.C. Attiogbé (France)


Formal Analysis, B, Theorem Proving, Model Checking.


Tool-assisted analysis of software systems and convenient guides to practise the formal methods are still motivating challenges. This article addresses these challenges. We ex periment on analysing a formal specification from multiple aspects. The B method and the Atelier-B tool are used for formal specifications, for safety property analysis and for refinements. The ProB tool is used to supplement the study with model checking; it helps to discover errors and there fore to improve the former specifications.

Important Links:

Go Back