7. B System or B Event

7.1 B extensions at system level

In order to be able to work on systems that are not as small as software, it is necessary to model the environment in addition to the strictly software part, which is not done by B software or B "classic", which works in a closed way. B event-driven or B system-driven (we'll use both terms interchangeably) responds to the problem of systems by taking into account the reactive aspect, where the environment acts on the system and vice versa. To this end, the concepts of software B or classical B have been generalized. State/transition modeling is proposed (as for automata), with a static part and a dynamic part. In static mode, i.e. at a given moment in time, the state of the system is presented in two aspects: on the one hand, the state of the software...