Exploration de techniques de modelisation et de verification logicielle en avionique

In recent years, the increasing use of software systems in aircrafts, the growth of their complexity and the application of strict norms defining the software development process have led to higher development costs. For this reason, new tools specializing in many parts of the software development process have come to the market. SCADE Suite from Esterel-Technologies is the perfect example of such a tool. Indeed, SCADE offers a formal programming language that can guarantee determinism, a simulator for testing, a qualified source code generator and some advanced verification possibilities such as a model test coverage tool and a formal proof engine.; The use of advanced verification techniques (formal proof, structural coverage) in a tool that addresses an important part of the critical software development process, like SCADE Suite, is a relatively new in the industry. In this project, a verification methodology, which respects the DO-178B's verification objectives, avionic's software development standard, will be proposed. The proposed methodology will allow the use of SCADE Suite's advanced verification tools.; The verification methodology is based on activities which address DO-178B's verification objectives. Those have been determined after an analysis of SCADE's possibilities, SCADE's proposed development methodology and after the chapter 6 of the DO-178B which discuss the software verification process.; The methodology has been tried on a software function from a real avionics project and compared to a more traditional methodology based solely on tests. This has shown the advantages in using the advanced verification tools. Those are: the diminution of unit tests, the detection of corner case bugs and the mathematical proof that some situations will never happen.; Furthermore, a usability experiment has showed that no productivity loss is associated with the use of SCADE's development methodology in comparison with a more traditional C methodology. This experiment, which tried to simulate an assignment to a new development project to the participants, was not able to show a productivity gain between any of the methodologies, notwithstanding that none had previous experience with SCADE and most had a lot of experience with the C language.; This project is an excellent introduction to the critical development process in avionics and to SCADE's possibilities.