6. B limits

Despite all these advantages, the classic B method is limited in a number of ways that are not related to the method itself. Figure 8 shows B's various interfaces with the environment, which consists of the natural language specification (B's input), the inputs (information acquired: other software, other ECUs, sensors, transmission media) and outputs (information supplied : to other software, other ECUs, actuators or means of transmission), application data and parameters in B, non-secure parts not realized in B, coding and compilation to obtain PROMs (read-only memory where the program to be executed by the industrial ECU is located if this is the case). These limitations mean that the proof cannot cover these points. It is therefore important to be aware of this, in order to put in place the additional...