Model Checking Ariane-5 Flight ProgramReport as inadecuate

Model Checking Ariane-5 Flight Program - Download this document for free, or read online. Document in PDF available to download.

1 VERIMAG - IMAG - VERIMAG 2 AST - Astrium Space Transportation

Abstract : 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.

Keywords : model-checking SDL IF mu-calculus properties validation methodology

Author: Marius Bozga - Laurent Mounier - David Lesens -



Related documents