Advances in Automotive System Modeling: EAST-ADL (Part 2): Page 2 of 7

May 24, 2013 //By DeJiu Chen, KTH; Lei Feng, Volvo; Henrik Lönn, Volvo; Juha-Pekka Tolvanen, MetaCase
Advances in Automotive System Modeling: EAST-ADL (Part 2)
For decades developers of automotive embedded systems have enjoyed the benefits of modeling. Models have not only served communication and gaining better understanding but are also used to prototype, analyze, simulate and test the developed systems. With dedicated generators it has also been possible to produce production-quality software code from the models. Typical cases of code generation are various control-engineering solutions and infotainment systems with HMI’s.

here .

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

Design category: 

Vous êtes certain ?

Si vous désactivez les cookies, vous ne pouvez plus naviguer sur le site.

Vous allez être rediriger vers Google.