G\'en\'eSyst : G\'en\'eration d'un syst\`eme de transitions \'etiquet\'ees \`a partir d'une sp\'ecification B \'ev\'enementiel

TL;DR

GénéSyst is a tool that automatically generates automata representing all behaviors of a formal specification, aiding in error detection and verification in formal development processes.

Contribution

It introduces GénéSyst, a novel tool that generates automata from B specifications, including refinement steps, to improve behavioral analysis and verification.

Findings

GénéSyst successfully generates automata covering all specification behaviors.

The tool incorporates refinement steps as sub-automata.

It enhances error detection in formal specifications.

Abstract

The most expensive source of errors and the more difficult to detect in a formal development is the error during specification. Hence, the first step in a formal development usually consists in exhibiting the set of all behaviors of the specification, for instance with an automaton. Starting from this observation, many researches are about the generation of a B machine from a behavioral specification, such as UML. However, no backward verification are done. This is why, we propose the GeneSyst tool, which aims at generating an automaton describing at least all behaviors of the specification. The refinement step is considered and appears as sub-automatons in the produced SLTS.