A credible autocoding application within a rocket and its payload

The cost of software engineering and avionics represents more than half of the budget of a safety-critical system like an aircraft or a UAV. The quantity and the complexity of embedded software in such systems is increasing exponentially. Reducing their cost of development is a major objective in the aeronautics and avionics industry. Research in Cyber Physical Systems (CPS) endeavours to contribute to this objective. The traditionnal approach to certifying software is to design unit tests to match low level requirements, and integration tests to validate high level requirements. Creating and running these tests require large amounts of time and money. With the recent bloom of companies specialized in UAV and small systems design, there is a need for new methods able to generate reliable codes in large projects easily, quickly, and in a cost efficient manner. Formal methods are a collection of techniques for the mathematical analysis of programs and models, which can assist in the certification of software with respect to FAA and EASA certification guidelines.