Marius Bozga, David Lesens, Laurent Mounier. Model-Checking Ariane-5 Flight Program. In Proceedings of FMICS'01 (Paris, France), Pages 211-227, 2001.
Download paper:
Adobe portable document (pdf)
Copyright notice:
This paper reports a verification experiment carried out on a re-engineered description of a part of Ariane-5 Flight Program. This is the embedded software which solely controls the Ariane-5 launcher during its flight, from the ground, through the atmosphere and up to the final orbit. In this case study, the SDL language was used to describe the main functional behavior of the flight program including the most relevant actions and their associated timing constraints, which are necessary to ensure the correct operation of the launcher. This description abstracts away both complex functionalities such as navigation and control algorithms and also implementation details, such as specific hardware and operating system dependencies. Several properties could then be verified on this specification using the IF toolbox, an open validation platform developed at Verimag for real-time asynchronous systems. The results obtained confirm that model-checking and complementary techniques (such as static analysis or abstraction), combined within a set of methodological guidelines, could be successfully applied to the validation of large real-time embedded systems
[ Model-based verification techniques ]
@InProceedings{Bozga-Lesens-Mounier-01,
Author = {Bozga, Marius and Lesens, David and Mounier, Laurent},
Title = {{M}odel-{C}hecking {A}riane-5 {F}light {P}rogram},
BookTitle = {Proceedings of FMICS'01 (Paris, France)},
Pages = {211--227},
Publisher = {INRIA},
Year = {2001}
}
Get EndNote Reference (.ref)