Please use this identifier to cite or link to this item:
Title: Runtime validation using interval temporal logic
Authors: D’Emanuele, Karlston
Pace, Gordon J.
Keywords: Computer programs -- Verification
Real-time data processing
Discrete-time systems
Computer software -- Development
Issue Date: 2006
Publisher: University of Malta. Faculty of ICT
Citation: D’Emanuele, K., & Pace, G. J. (2006). Runtime validation using interval temporal logic. 4th Computer Science Annual Workshop (CSAW’06), Bighi. 1-7.
Abstract: Formal specifications are one of the design choices in reactive and/or real-time systems as a number of notations exist to formally define parts of the system. However, defining the system formally is not enough to guarantee correctness thus the specifications are used as execution monitors over the system. A number of projects are around that provides a framework to define execution monitors in Interval Temporal Logic (ITL), such as Temporal-Rover, EAGLE Flier, and D3CA framework. This paper briefly describes the D3CA framework, consisting in the adaptation of Quantified Discrete-Time Duration Calculus to monitoring assertions. The D3CA framework uses the synchronous data-flow programming language Lustre as a generic platform for defining the notation. Additionally, Lustre endows the framework with the ability to predetermine the space and time requirements of the monitoring system. After defining the notation framework the second part of the paper presents two case studies - a mine pump and an answering machine. The case studies illustrate the power endowed by using ITL observers in a reactive or event-driven system.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
Proceedings of CSAW'06 - A21.pdf232.15 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.