Behavior-Preserving Abstraction of ESTEREL Programs

• Autorzy: Nir Koblenc , Shmuel Tyszberowicz
• Języki publikacji: EN

Abstrakty

EN

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.(original abstract)

Słowa kluczowe

EN

Programing languages; Verification of knowledge; Computer systems

PL

Języki programowania; Weryfikacja wiedzy; Systemy komputerowe

• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2015
• Tom: 5
• Strony: 743--754

Twórcy

autor

Nir Koblenc

• Open University of Israel

autor

Shmuel Tyszberowicz

• Academic College of Tel-Aviv Yaffo

Bibliografia

• N. Koblenc, "Purification of Esterel Programs," Master's thesis, Dept. Mathematics and Computer Science, Open Univ. of Israel, Ra'anana, Israel, June 2015, the thesis and prototype tool are available at http://www.cs.tau.ac.il/~tyshbe/NIR/nirThesis.html.
• N. Koblenc and S. Tyszberowicz, "Purification of Esterel Programs," in Preproceedings of the Brazilian Symp. on Formal Methods (SBMF), C. Braga and N. Martì-Oliet, Eds., 2014, pp. 183-188, available at: http://www2.ic.uff.br/~cbraga/sbmf14/sbmf14-preproceedings.pdf (visited September 2015).
• N. Halbwachs, Synchronous Programming of Reactive Systems, Stankovic, J. A. (Consulting Editor), Ed. Kluwer, 1993. [Online]. Available: http://dx.doi.org//10.1007/978-1-4757-2231-4
• G. Berry, "The Esterel v5 Language Primer, Version v5_91," Centre de Mathématiques Appliquées - Ecole des Mines and INRIA, 06565 Sophia-Antipolis, 2000.
• L. J. Jagadeesan, C. Puchol, and J. E. von Olnhausen, "A formal approach to reactive systems software: a telecommunications application in Esterel," Formal Methods in System Design, vol. 8, no. 2, pp. 123- 151, 1996. [Online]. Available: http://dx.doi.org/10.1007/BF00122418
• I. Sommerville, Software Engineering, 8th ed. Addison-Wesley, 2007.
• A. Bouali, "XEVE, an Esterel verification environment," in Computer Aided Verification (CAV), ser. LNCS, A. J. Hu and M. Y. Vardi, Eds., vol. 1427. Springer-Verlag, 1998, pp. 500-504. [Online]. Available: http://dx.doi.org/10.1007/BFb0028770
• "The Esterel v7 Reference Manual, Version v7_30 - initial IEEE standardization proposal," Esterel Technologies, 2005.
• G. Berry and the Esterel Team, The Esterel v5_91 System Manual, Centre de Mathématiques Appliquées - Ecole des Mines de Paris / INRIA, Sophia-Antipolis, 2000.
• S. Das, D. L. Dill, and S. Park, "Experience with predicate abstraction," in Computer Aided Verification (CAV), ser. LNCS, N. Halbwachs and D. Peled, Eds., vol. 1633. Springer, 1999, pp. 160-171. [Online]. Available: http://dx.doi.org/10.1007/3-540-48683-6_16
• J. L. Jones and D. Roth, Robot Programming: A Practical Guide to Behavior-Based Robotics. McGraw-Hill, 2003.
• B. Alpern, M. N. Wegman, and F. K. Zadeck, "Detecting equality of variables in progress," in Principles of Programming Languages (POPL 1988). ACM, 1988, pp. 1-11. [Online]. Available: http: //dx.doi.org/10.1145/73560.73561
• A. Benveniste and G. Berry, "The synchronous approach to reactive and real-time systems," Proceedings of the IEEE, vol. 79, no. 9, pp. 1270-1282, September 1991. [Online]. Available: http: //dx.doi.org/10.1109/5.97297
• G. Berry and G. Gonthier, "The Esterel synchronous programming language: design, semantics, implementation," Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992. [Online]. Available: http://dx.doi.org/10.1016/0167-6423(92)90005-V
• G. Dudek and M. Jenkin, Computational Principles of Mobile Robotics. Cambridge University Press, 2000.
• G. Berry, The Constructive Semantics of Pure Esterel, 2002, draft book, version 3, available at: http://www-sop.inria.fr/members/Gerard. Berry/Papers/EsterelConstructiveBook.pdf (visited September 2015).
• C. Puchol, The TempEst Program Verification Toolset, AT&T Bell Laboratories and the University of Texas at Austin, product documentation.
• L. J. Jagadeesan, C. Puchol, and J. E. Von Olnhausen, "Safety property verification of Esterel programs and applications to telecommunications software," in Computer Aided Verification (CAV), ser. LNCS, P. Wolper, Ed., vol. 939. Springer-Verlag, 1995, pp. 127-140. [Online]. Available: http://dx.doi.org/10.1007/3-540-60045-0_45

Identyfikatory

DOI

10.15439/2015F190