Abstract:
Esterel is a synchronous programming language dedicated to the development of reactive systems. Reactive programs are often used to control safety-critical systems; therefore rigorous design methods and formal verification are considered. While verifying a model of the system has many benefits, the product code may contain errors.

In this lecture I’ll describe an automatic abstraction process for Esterel programs that results in a pure-Esterel program with an equal observable behavior, by eliminating variables, sensors, valued signals, and literals. When applying this abstraction to a program augmented with observers that monitor safety properties, the resulting pure program can be compiled using an Esterel compiler and then verified using tools such as Xeve. The abstraction algorithm and the tool based on it are applicable to various examples of control programs and robotic systems.