Requirements & Problem Frames Model of SSE. To develop the requirements of the SSE the limitations and borders of the system have to be clear. We concentrate only on the software part of the system. A real SSE affects not only the software part of the car. We illus- trate this with an example: The engine of a car with a SSE is started and stopped more often than an engine of a car without a SSE. The starter has to be capable of this additional requirement. Therefore the development of a complete SSE must include the requirements for the surrounding systems (see Section 2.2). We assume for the enhanced development that these requirements are treated elsewhere and concentrate only on the software part. For both the Problem Frames model and the requirements document assump- tions have to be made. An example of such an assumption is the following Every error concerning the vehicle (accident, sensor error,. . . ) is detected by the error handling of the car. This assumption ensures that it is enough to include the error handling in the model of the SSE to address all kinds of errors. Time and Timing Constraints Before we illustrate the requirements document, the Problem Frames model and the invariants, we address one important aspect for all of them. Time and timing constraints play an important role, but they have to be adjusted to the different system borders. In the requirements document and the Problem Frames model time and timing constraints address real physical phenomena. A (simplified) example would be The engine must change the status from off to running within time t if the battery charging state is below a defined limit Para Battery. To fullfill this requirement a sensor has to check the battery charging state, pass the information to the SSE, the SSE has to check if it is be- low the defined limit Para Battery and in this case send an order to start the engine to the engine control, which has to start the engine, which again needs some time. For the requirements it is convenient to address the real world phenomena, but when translating these requirements into invariants for Event-B timing constraints have to be carefully considered. The Event-B model only considers the time between the information reaches the SSE and the output leaves the SSE. Therefore timing constraints have to be adjusted. Within the SSE time is needed to produce an output according to the in- put. The events in the Event-B model are ordered and when formulating the invariant one has to consider this order which depends ...
