Modular Distribution and Application to Discrete Controller Synthesis
Gwenaël Delaval, Inria Grenoble · 2008
This paper shows the application of the automatic distribution of synchronous reactive programs to the specic problem of discrete controller synthesis of complex reactive systems. Discrete controller synthesis is a formal method used to ensure properties on a exible system which does not a priori verify them. However, this method is ecient only on Boolean programs. More complex embedded systems, comprising complex data types and structures, cannot be addressed without abstraction means. We show how such abstractions can be obtained automatically using a type-directed projection operation. This operation allows then the safe recombination of the result of the synthesis with the original abstracted system, preserving the ensured properties.