Towards the Safety Verification of Real-Time Systems with the Coq Proof Assistant

• Autorzy: Tveretina O.
• Języki publikacji: EN

Abstrakty

EN

Hybrid systems involve the interaction of discrete and continuous dynamics. Hybrid systems have been used as a mathematical model for many safety critical applications. One of the most important analysis problems of hybrid systems is the reachability problem. In this paper we argue that the proof assistant Coq can be used for the hybrid systems verification. An example of a train crossing control is provided.

Słowa kluczowe

EN

formal methods; real-time; theorem proving

• Wydawca: Łukasiewicz Industrial Research Institute for Automation and Measurements PIAP
• Czasopismo: Journal of Automation Mobile Robotics and Intelligent Systems
• Rocznik: 2009
• Tom: Vol. 3, No. 1
• Strony: 30--32
• Opis fizyczny: Bibliogr. 6 poz.

Twórcy

autor

Tveretina O.

• Institute for Computing and Information Sciences, Radboud University Nijmegen, The Netherlands,

Bibliografia

• [1] R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, A. Olivero, J. Sifakis, S.Yovine, “The algorithmic analysis of hybrid sys-tems”, Theoretical Computer Science, vol. 138, 1995, pp. 3-34.
• [2] R. Alur, Th.Dang, F.Ivancic, “Reachability Analysis of Hybrid Systems via Predicate Abstraction”, ACM transactions on embedded computing systems (TECS), 2004.
• [3] Y. Bertot, P. Casteran, “Interactive Theorem proving and Program Development”, Springer, 1998.
• [4] T.A. Henzinger, X. Nicollin, J. Sifakis, S.Yovine, “Symbolic Model Checking for Real-time Systems", 7th Symposium of Logics in Computer Science, 1992.
• [5] A. Henzinger, P.W. Kopke, A. Puri, P. Varaiya, “What's Decidable About Hybrid Automata?”, Journal of Computer and System Sciences, vol. 57, no. 1, 1998, pp. 94-124.
• [6] S. Ratschan, Z. She, “Safety verification of hybrid systems by constraint propagation-based abstraction refinement”, ACM Transactions on Embedded Computing Systems (TECS), vol. 6(1), 2007.