Application name:

Digital Control Unit (DCU)

Organisation:

SNECMA Systems, European SACRES Project (EP20897)

Method:

Synchronous language SIGNAL

Tools:

TNI/SILDEX v4 (design and code generation)
System Verification Tools : AHL/Timing Diagram Editor; SIEMENS/System Verification Environnement; OFFIS/Proof manager toolset

Domain:

The DCU is an airframe mounted electronic package with microprocessor based programmable digital control. The function of the DCU is to provide control of turboshaft engine (Helicopter) in order to obtain a safe steady state and a transient engine performance. It shall provide full authority control of fuel flow and power matching, combined with a manual backup.

Period:

1996-1998

Size:

Model containing 20 statecharts

Description:

Siemens is using the SVE model checker in a number of inhouse applications. This application was done in cooperation with Renault. It controls the speed of a car. It contains control and regulation parts which are both modelled using statecharts but can be separated easily from each other. A list of safety critical properties resulting from a safety analysis has been supplied to SIEMENS Corporate Technology by Technocentre Renault. These properties have been checked fully automatically using the SVE modelchecker developed by Siemens Corporate Technology. The SVE modelchecker checks given properties for a Statemate model fully automatically. In the case that a property does not hold for the given model SVE produces a countersequence, i.e. a execution sequence of the model which violates the property.

Conclusions:

Due to the full automation SVE allows the user to verify a Statemate model with little additional effort and with almost no knowledge of formal verification. In this case study a complicated error has been found which hardly would have been detected by testing. Currently, the verification is limited to finite-state models, i.e. the control logic. Yet this case study demonstrates that even in a domain involving real-valued parameters, all relevant properties are independent of the numerical computations, and could therefore be analysed.

Publications:

None.

Contact:

Name:	Martin Weiss
Organisation:	SIEMENS Corporate Technology
Address:	Design Automation SIEMENS Corporate Technology D-81730 Munich
Country:	Germany
Phone number:	+49 (89) 636-41743
Fax:	+49 (89) 636-42284
E-mail:	Martin.Weiss@mchp.siemens.de
Personal website:	http://www.tni.fr/sacres/

URL:

http://www.tni.fr/sacres/

Remarks:

The work was performed within the ESPRIT project SACRES - Safety Critical Embedded Systems.

© copyright 2004 | Formal Methods Europe