Fluent temporal logic for discrete-time event-based models

File Description SizeFormat 
synchronous-fltl.pdfAccepted version308.42 kBAdobe PDFDownload
Title: Fluent temporal logic for discrete-time event-based models
Author(s): Letier, E
Kramer, J
Magee, J
Uchitel, S
Item Type: Conference Paper
Abstract: Fluent model checking is an automated technique for verifying that an event-based operational model satisfies some state-based declarative properties. The link between the event-based and state-based formalisms is defined through fluents which are state predicates whose value are determined by the occurrences of initiating and terminating events that make the fluents values become true or false, respectively. The existing fluent temporal logic is convenient for reasoning about untimed event-based models but difficult to use for timed models. The paper extends fluent temporal logic with temporal operators for modelling timed properties of discrete-time event-based models. It presents two approaches that differ on whether the properties model the system state after the occurrence of each event or at a fixed time rate. Model checking of timed properties is made possible by translating them into the existing untimed framework. Copyright 2005 ACM.
Publication Date: 1-Dec-2005
URI: http://hdl.handle.net/10044/1/5890
Publisher Link: http://doi.acm.org/10.1145/1095430.1081719
ISBN: 1-5959-3014-0
Publisher: ACM
Presented At: ESEC-FSE 2005, the Joint 10th European Software Engineering Conference
Published Proceedings: Proceedings of the 10th European software engineering conference
Start Page: 70
End Page: 79
Copyright Statement: © ACM, 2005. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in PROCEEDINGS OF THE 10TH EUROPEAN SOFTWARE ENGINEERING CONFERENCE,(2005) http://doi.acm.org/10.1145/1095430.1081719
Conference Location: Lisbon, Portugal
Appears in Collections:Distributed Software Engineering

Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons