 |
|
Application name:
Data Management System (DMS) Design Validation (DDV)
Organisation:
Work developed under contract for the European Space Agency (ESA), by a consortium made up of:
Matra Marconi Space (prime contractor, Toulouse, France); Dornier (Friedrichshafen, Germany); Verimag (Grenoble, France)
Method:
SDL
Tools:
Geode and CADP (Caesar/Aldebaran Development Package)
Domain:
Real-Time Control and Data Handling systems
Period:
1995 - 1996
Size:
6200 SDL lines
Description:
The DDV study address the design validation in the early system lifecycle using formal methods, with the following steps:
- the collection and informal expression of user requiremenst, derived from the analysis of a particular space mission.
- the system specification description and logical verification,
- the architectural design description , logicl verification and performance analysis.
The efforts were concentrated on the the use of a provable and formal specification method for the verification of specification, and to demonstrate that an error free transmission can be be done to the architectural design. It was applied to a critical component of a space system, the Fault Detection Isolation and Recovery (FDIR).
Conclusions:
A tentative classification of formal methods was proposed, based on the definition of a set of criteria to characterise the method, the application and the tools. The criteria are marked according to the importance they are given in the current project, they are then weighted and allow to give a final classification of the methods and tools for the application in the project. In DDV for an FDIR application, SDL was first ranked, specially when associated with Workbench for the performance verification.
A specification model of the system was developed by Matra and safety properties were verified. The safety properties, derived from the system FMECA, were expressed in MSCs, or logical assertions, or with injectors/observers. The ALDEBARRAN tool of Verimag was used to reduce the complex model to a simple automaton modulo a reduced set of visible events.
The model was transferred to Dornier for architectural design. The knowledge transfer of the system was highly improved by the use of the model. A design model was developped in SDL, and it was showed equivalent to the specification model with CADP (modulo the same set of observable events). Then the performance model was developped with Workbench, coupled with ObjectGeode in the EasySim tool. The performance properties were checked with the tools.
A design error was found during the verification. It would only have been possible to correct it at integration level, and this would have cost around 500KECU, while the investment cost in the modelisation activity was less than 100 KECU (licence, training, development). The return on investment has been demonstrated.
Publications:
DMS Design Validation Final Report ESA 9558/91/NL/JG
Contact:
| Name: | Joseph Sifakis |
| Organisation: | Verimag Gieres |
| Address: | Grenoble |
| Country: | France |
| Phone number: | +33 (4) 76634848 |
| E-mail: | Joseph.Sifakis@imag.fr |
Contact:
| Name: | Philippe Humbert or Eric Conquet |
| Organisation: | Matra Marconi Space |
| Address: | Toulouse |
| Country: | France |
| Phone number: | +33 (5) 62196219 |
|
