On the Polychronous Approach to Embedded Software Design

Formal approaches for designing mission critical embedded software are gaining importance due to the complexity of concurrent nature and the asynchronous interaction with the environment by such software. "After-the-fact" formal verification is one way to provide correctness guarantees, but is plagued with state-space explosion and other problems. "Correct-by-construction" design approach is therefore often the methodological choice for such software design. Polychronous or "multi-clock" model of computation (MoC) in the context of synchronous programming has been successfully used in many safety critical embedded software design in avionics, and other industries in France. SIGNAL is an example Of Such an embedded software system description language that captures a polychronous MoC. SIGNAL compiler generates deterministic embedded software with provable properties from polychronous specifications. However, an embedded software often interacts with operating systems, hardware interrupt controllers, and other software applications. Therefore, determinism itself may not provide enough guarantee for the correct operation of a software component designed this way. Tighter characterizations beyond determinacy have been invented to guarantee safe usage of such software in an embedded context with lesser restrictive requirements on the environment. "Endochrony" is one such characterization, which is often hard to understand by regular embedded software designers due to the complications of the semantic domain in which such characterization has been expressed in the past. In this paper we provide a true concurrency based semantics which we believe makes the notion of endochrony easier for real system engineers to comprehend and use as a technique to guarantee usage safety.