Polychronous Design of Embedded Real-Time Systems

This report proposes a design methodology for embedded real-time systems using a synchronous multi-clocked framework, which provides a well-defined mathematical model that yields rigorous methodological support for the trusted design, validation and automatic code generation. The presented methodology addresses among others the non trivial issue of modeling asynchronous mechanism using the synchronous paradigm. Among target application domains, we mainly focus on the avionics area. A library of polychronous models of services has been implemented, based on the avionic standard APEX-ARINC 653. These services describe functionalities of a real-time operating system in integrated modular avionics architectures. The proposed methodology has been applied to some case studies in avionics. The library is also the basis for another study that consists of modeling Real-Time Java applications in the polychronous framework. A great advantage is that formal transformation and optimization techniques become enabled. Finally, a major contribution of the work exposed in this report is the convergence between the theory of formal methods, industrial practice and current trends in embedded real-time system design