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

TL;DR

This paper demonstrates a multi-facet analysis approach for formal specifications using Atelier-B for safety and refinement, complemented by ProB model checking to identify errors and enhance the specifications.

Contribution

It introduces a combined methodology leveraging Atelier-B and ProB tools for comprehensive analysis of formal specifications from multiple perspectives.

Findings

ProB helps discover errors in formal specifications.

Combined tool approach improves specification quality.

Analysis from multiple aspects enhances understanding of specifications.

Abstract

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.