Semantics-Preserving Design of Embedded Control Software from Synchronous Models

While the complexity of embedded systems is constantly ramping up, dealing with concurrency has become increasingly difficult. As a consequence, the interest in mathematical models has grown considerably due to the availability of industrial tools and of a large body of theoretical results. Numerous mathematical models of computation have been proposed, each exploiting a particular trade-off between analytical power and constraints imposed on the final implementation. Some models, such as the event-driven models, imply a very limited set of constraints on the final implementation and are, therefore, well-suited for software implementation. On the other hand, time-driven models are of great interest because of the strong properties that can be verified formally. Synchronous languages, such as ESTEREL, LUSTRE, and SIGNAL, are among the most successful time-driven models. Design environments, such as Simulink and SCADE, are examples of the analytical power provided by time-driven models. Synchronous languages, built on the so-called “synchronous programming model”, are based on the “synchronous assumption”, providing an effective and rigorous way of dealing with concurrency but imposing, at the same time, strong constraints on the final implementation. As a result, it becomes very difficult to rigorously and efficiently implement synchronous programs on the available implementation platforms.