Behavior-Preserving Abstraction of Esterel Programs
Nir Koblenc, Shmuel Tyszberowicz
DOI: http://dx.doi.org/10.15439/2015F190
Citation: Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 5, pages 743–754 (2015)
Abstract. Reactive programs often control safety-critical systems, thus it is essential to verify their safety requirements. Esterel is a synchronous programming language for developing control-dominated reactive systems, and XEVE is a verification environment that analyzes circuit descriptions generated from Esterel programs. However, a circuit generated by the Esterel compiler from non-pure Esterel program often displays behaviors which may violate safety properties even when the source program does not. We introduce an automatic abstraction process for Esterel programs developed to tackle this problem. When the process is applied to a program augmented with observers to monitor the program's behavior, it results in a pure program that preserves the behavior of the source program, replacing value-carrying objects with pure signals. We have built a prototype tool that implements the abstraction and used it to purify control programs and robotic systems.