Figure 11 shows the related computation constraints on the ABS function. The specification declares two allowed invocations to the transformation Set_ABSBrakeTorqueOut() that calculates the ABS brake torque request.
Figure 11. Annotating computation constraint on the ABS function. For full resolution click here .
In regards to the execution of application functions, EAST-ADL, through its timing model, enables specifying the mapping of overall timing constraints to the timing properties of individual functions for multitasking. For each system function such timing properties include the preferred triggering policy (e.g. time- or event-triggered) and related timing constraints (e.g. response time, precedence and synchronization). If triggered, each system function runs according to a run-to-completion semantics.
EAST-ADL aims to obtain most of its analytical leverage through well established analysis methods and tools. To this end, the support for model transformations from EAST-ADL behaviour models to external analysis tools includes SPIN, UPPAAL, Matlab/Simulink and Modelica.
Let’s consider an example of exhaustively verifying the behavioural model against requirements with the model checker SPIN. The verifiable requirements include assertion, freedom of deadlock, reachability of the desired state, avoidance of or compliance with given execution patterns, and linear temporal logic (LTL) statements. We have defined the generic mapping rules between EAST-ADL behaviour constructs and PROMELA language used to specify SPIN models.
The mapping rules are implemented as an algorithm in MetaEdit+ to automatically transform the behaviour model of EAST-ADL into the SPIN model. Figure 12 shows the PROMELA code section of the ABS function. The assertion statement assert(0) guides SPIN to search the execution path to reach the statement and the path indicates the locked condition of a wheel. In model checking terminology, the path is a counterexample, which gives the designer the hint on how the given state may be reached.
Figure 12. The PROMELA Code Section of the ABS Function. For full resolution click here.
To illustrate the analysis leverage through SPIN, the verification result on