this assertion is shown in Figure 13, with the screen snapshot of the SPIN printout. The top line shows the version of the SPIN model checker and the following two lines the applied algorithm options. At the lower section can we see the memory usage of this verification: the actual usage is 154 MB. The last line indicates the execution time, i.e., 4.63 seconds. The reader who is unfamiliar with SPIN may conveniently ignore other details. The counter example can be visualized by SPIN through both tracking variable values and examining process communication via a message sequence chart. The locking condition identified in Figure 13 occurs when the wheel speed is reduced by the brake torque but the latest vehicle speed estimate has not been calculated and broadcasted to the wheels. This scenario is possible in the current architecture because the processes are asynchronous and may occur in any order. If one wants to ensure that the ABS function always receives the latest speed estimate before making the control decision, a stricter execution and communication protocol must be enforced in the software architecture.
Figure 13. SPIN Verification Result. For full resolution click here .
Besides the assertion in the ABS function, we can check many other properties of the entire brake system, including the ABS function, driver’s brake command, wheel and vehicle body dynamics.
As an overall system property, safety is concerned with faults and failure cases and how they influence to the system. EAST-ADL aims to express precisely the safety requirements and related information along with the nominal system model in all the phases covered by the ISO 26262 reference safety lifecycle. This means that for any safety requirement EAST-ADL provides support for specifying its allocation, precise meaning, and integrity level based on the ASIL (Automotive Safety Integrity Level) classification scheme of ISO/DIS 26262.
EAST-ADL covers the specifications of safety requirements as well as their system dependability