PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

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

Autorzy
Treść / Zawartość
Identyfikatory
Warianty tytułu
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
Twórcy
autor
  • Institute for Computing and Information Sciences, Radboud University Nijmegen, The Netherlands, o.tveretina@cs.ru.nl
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.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUJ6-0023-0144
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.