Towards the verification of real-time systems in avionics
B. Berthomieu, Pierre-Olivier Ribet, François B. Vernadat, J.L. Bernartt, J-M. Farines, J.-P. Bodeveix, Mamoun Filali, Gérard Padiou, Pierre Michel, Patrick Farail, P. Gauffilet, Pierre Dissaux, J.E. Lambert · Electronic Notes in Theoretical Computer Science · 2003
The Cotre Project1 is aimed at providing a design methodology and an associated software environment for the development of embedded realtime avionic systems. It contributes to bridging the gap between requirements of such systems, typically expressed in Architecture Description Languages, and formal development techniques, relying on system modeling and verification. This paper presents the current status of the language and platform adopted in Cotre project. The need for using various formalisms leads us to adopt an intermediate language. We describe this language, its translation in the chosen formalisms and present an application example.