Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications

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...

Full description

Bibliographic Details
Main Authors: Erika Ábrahám, Peter Csaba Ölveczky, Daniela Lepri
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
id doaj-c886454a8d3144088c750291acf0d813
record_format Article
spelling doaj-c886454a8d3144088c750291acf0d8132020-11-24T22:04:19ZengOpen 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
collection DOAJ
language English
format Article
sources DOAJ
author Erika Ábrahám
Peter Csaba Ölveczky
Daniela Lepri
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
author_facet Erika Ábrahám
Peter Csaba Ölveczky
Daniela Lepri
author_sort Erika Ábrahám
title 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_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_sort model checking classes of metric ltl properties of object-oriented real-time maude specifications
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2010-09-01
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.
url http://arxiv.org/pdf/1009.4264v1
work_keys_str_mv AT erikaabraham modelcheckingclassesofmetricltlpropertiesofobjectorientedrealtimemaudespecifications
AT petercsabaolveczky modelcheckingclassesofmetricltlpropertiesofobjectorientedrealtimemaudespecifications
AT danielalepri modelcheckingclassesofmetricltlpropertiesofobjectorientedrealtimemaudespecifications
_version_ 1725829304268357632

Similar Items