Integration of ProB

ProB model-checker is being integrated in Atelier B 4.0, in order to provide additional proof power and animation capabilities to Atelier B.

With the help of Pr. Michael Leuschel, a MacOS prototype has been developped, allowing to animate and model-check a B model from Atelier B 4.0. At that occasion, a generic interfacing mechanism has been developped and will be enriched and improved in the future. This mechanism is described in the GUI_Project section. ProB 1.3.0+ is now self integrating with AtelierB 4.0, at model level. Ongoing developments at University of Dusseldorf for integration at proof obligation level.

Ce contenu a été publié dans Research, Tools. Vous pouvez le mettre en favoris avec ce permalien.

Laisser un commentaire