Author(s)

LIU NING, WANG KEMING, HOU XILI, WANG XIA, CHENG PENG

Abstract

This article presents our experience in developing a tram control system using the B formal method. We find that there are some notable issues when using an abstract machine model to express software systems and in automatic code generation, for which we have summarized the solutions. In this paper, we illustrate how to use the B module to develop complex systems, the rational choice of implication relations of the invariants, as well as the correctness of the variable definition in the model for code generation. The solutions to these issues can help developers with less experience to better use the B method to develop the reliable systems.

Keywords

B method, invariant, modelling, code generation, application exploration