Modelling and Validating an Automotive System in Classical B and Event-B

Abstract

We have modelled parts of the ABZ automotive case study using the B-method. For the early phases of modelling we have used the classical B for software, while for proof we have used Event-B and Rodin. It is maybe surprising that classical B’s machine inclusion mechanism along with operation calls can be used for modular system modelling. Moreover, for one particular style of modelling, the result can then be translated to superposition refinement with event extension in Event-B. Before conducting the proof, we have validated our models using model checking and animation with visualizations. The graphical visualizations were constructed using a new plugin (VisB) which helped uncover errors and transforms our model into an executable, interactive reference specification which can be examined by users without formal background.

Document

Reference

% BibTex
@inproceedings{leuschel2020abz,
  title={{Modelling and Validating an Automotive System in Classical B and Event-B}},
  author={Leuschel, Michael and Mutz, Mareike and Werth, Michelle},
  booktitle={7th International Conference on Rigorous State Based Methods (ABZ'20)},
  pages={335--350},
  year={2020},
  organization={Springer}
}

Sources

• Used formal method: Classical B Event-B

• Resources and tools: VisB

  For more information, please contact the authors