Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications
This paper presents a transformational approach for model checking two important classes of metric temporal logic (MTL) properties, namely, bounded response and minimum separation, for nonhierarchical object-oriented Real-Time Maude specifications. We prove the correctness of our model checking algo...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2010-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1009.4264v1 |
| _version_ | 1818346857023143936 |
|---|---|
| author | Erika Ábrahám Peter Csaba Ölveczky Daniela Lepri |
| author_facet | Erika Ábrahám Peter Csaba Ölveczky Daniela Lepri |
| author_sort | Erika Ábrahám |
| collection | DOAJ |
| description | This paper presents a transformational approach for model checking two important classes of metric temporal logic (MTL) properties, namely, bounded response and minimum separation, for nonhierarchical object-oriented Real-Time Maude specifications. We prove the correctness of our model checking algorithms, which terminate under reasonable non-Zeno-ness assumptions when the reachable state space is finite. These new model checking features have been integrated into Real-Time Maude, and are used to analyze a network of medical devices and a 4-way traffic intersection system. |
| first_indexed | 2024-12-13T17:24:55Z |
| format | Article |
| id | doaj.art-c886454a8d3144088c750291acf0d813 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-13T17:24:55Z |
| publishDate | 2010-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-c886454a8d3144088c750291acf0d8132022-12-21T23:37:12ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802010-09-0136Proc. RTRTS 201011713610.4204/EPTCS.36.7Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude SpecificationsErika ÁbrahámPeter Csaba ÖlveczkyDaniela LepriThis paper presents a transformational approach for model checking two important classes of metric temporal logic (MTL) properties, namely, bounded response and minimum separation, for nonhierarchical object-oriented Real-Time Maude specifications. We prove the correctness of our model checking algorithms, which terminate under reasonable non-Zeno-ness assumptions when the reachable state space is finite. These new model checking features have been integrated into Real-Time Maude, and are used to analyze a network of medical devices and a 4-way traffic intersection system.http://arxiv.org/pdf/1009.4264v1 |
| spellingShingle | Erika Ábrahám Peter Csaba Ölveczky Daniela Lepri Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications Electronic Proceedings in Theoretical Computer Science |
| title | Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications |
| title_full | Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications |
| title_fullStr | Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications |
| title_full_unstemmed | Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications |
| title_short | Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications |
| title_sort | model checking classes of metric ltl properties of object oriented real time maude specifications |
| url | http://arxiv.org/pdf/1009.4264v1 |
| work_keys_str_mv | AT erikaabraham modelcheckingclassesofmetricltlpropertiesofobjectorientedrealtimemaudespecifications AT petercsabaolveczky modelcheckingclassesofmetricltlpropertiesofobjectorientedrealtimemaudespecifications AT danielalepri modelcheckingclassesofmetricltlpropertiesofobjectorientedrealtimemaudespecifications |