Please use this identifier to cite or link to this item:
|Title:||Runtime validation using interval temporal logic|
Pace, Gordon J.
|Keywords:||Computer programs -- Verification|
Real-time data processing
Computer software -- Development
|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:
|Proceedings of CSAW'06 - A21.pdf||232.15 kB||Adobe PDF||View/Open|
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.