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

Szczegóły
Opis

Tytuł:: Towards the Safety Verification of Real-Time Systems with the Coq Proof Assistant
Autorzy:: Tveretina, O.
Powiązania:: https://bibliotekanauki.pl/articles/384877.pdf
Data publikacji:: 2009
Wydawca:: Sieć Badawcza Łukasiewicz - Przemysłowy Instytut Automatyki i Pomiarów
Tematy:: formal methods
real-time
theorem proving
Źródło:: Journal of Automation Mobile Robotics and Intelligent Systems; 2009, 3, 1; 30-32
1897-8649
2080-2145
Język:: angielski
Prawa:: CC BY-SA: Creative Commons Uznanie autorstwa - Na tych samych warunkach 3.0 PL
Dostawca treści:: Biblioteka Nauki
: Artykuł

Przejdź do źródła

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.

Informacja

Powiązane pozycje