Academic Journals Database
Disseminating quality controlled scientific knowledge

On Safety Properties and Their Monitoring

ADD TO MY LIST
 
Author(s): G. Rosu

Journal: Scientific Annals of Computer Science
ISSN 1843-8121

Volume: 22;
Issue: 2;
Start page: 327;
Date: 2012;
VIEW PDF   PDF DOWNLOAD PDF   Download PDF Original page

Keywords: runtime verification | monitoring | safety properties

ABSTRACT
This paper addresses the problem of runtime verification from a foundational perspective, answering questions like ``Is there a consensus among the various definitions of a safety property?'' (Answer: Yes), ``How many safety properties exist?'' (Answer: As many as real numbers), ``How difficult is the problem of monitoring a safety property?'' (Answer: Arbitrarily complex), ``Is there any formalism that can express all safety properties?'' (Answer: No), etc. Various definitions of safety properties as sets of execution traces have been proposed in the literature, some over finite traces, others over infinite traces, yet others over both finite and infinite traces. By employing cardinality arguments and a novel notion of {em persistence}, this paper first establishes the existence of bijective correspondences between the various notions of safety property. It then shows that safety properties can be characterized as ``always past'' properties. Finally, it proposes a general notion of {em monitor}, which allows to show that safety properties correspond precisely to the monitorable properties, and then to establish that monitoring a safety property is arbitrarily hard.
Why do you need a reservation system?      Save time & money - Smart Internet Solutions