Real-time systems are devices consisting of hardware and software with functional and timing constraints for the interaction with their environment. Telecommunication, nuclear power plants, avionics, and medical technology are typical domains where such systems are encountered. These systems are often critical because of the high human and economic stakes. Therefore, the development of these systems requires highly reliable methods. The synchronous approach has been proposed in order to answer this demand. Its mathematical basis provides a formal framework that favors the description and validation of real-time systems. The multi clock or polychronous model stands out from other synchronous speci cation models by the fact that it allows the description of systems where each component can have its own activation clock. Besides formal validation, it favors component-based approaches and modular development of large-scale systems. This document suggests a methodology for the design of real-time systems that uses as formalism the synchronous language Signal which relies on the polychronous model. It uses the formal tools and techniques based on this model in order to verify both behavioral and non functional properties. This facilitates design space exploration. The methodology presented here allows to design systems that contain asynchronous mechanisms using the synchronous approach. It illustrates the characterization of real-time behaviors in the polychronous model. Avionics is considered as privileged application domain in the current document. This work has been supported by the european project SafeAir (Advanced Design Tools for Aircraft Systems and Airborne Software) in which many industrials are involved. We especially are interested in the design of applications following the Integrated Modular Avionics (IMA) architecture model that is based on the avionic standard ARINC. This leads to the implementation of a library in Signal containing real-time executive services de fined by ARINC.
