Automatiser les preuves d'un sous-langage de la méthode B
Cet article propose une méthode pour automatiser les preuves pour un sous-langage
de la méthode B, en utilisant un prouveur dédié. Nous définissons d’abord le langage, puis exposons
la stratégie du prouveur associé, et son implantation au sein de l’Atelier B. Nous étudions
ensuite les propriétés du prouveur. Un exemple réel d’application industrielle est exposé pour
illustrer le processus.
This article illustrates the automatisation of proofs for a sub-language of the B
method, by using a dedicated prover. First, we define the language, then we explain the strategy
of its prover, and the implementation within the tool Atelier B. Next, we study the properties of
the prover. A real example of industrial application is exposed to illustate the process.
O.BOITE
preuve automatique, méthode B, vérification d’invariants ferroviaires.
automatic proof, B method, railway interlocking verification.
Français
|
