# Difference between revisions of "Efficient Monitoring of Safety Properties"

From FSL

Line 1: | Line 1: | ||

+ | == Journal of STTT == | ||

<pub id='havelund-rosu-2004-sttt' template='PubDefaultWithAbstractAndTitle'> </pub> | <pub id='havelund-rosu-2004-sttt' template='PubDefaultWithAbstractAndTitle'> </pub> | ||

+ | == TACAS'02 == | ||

+ | <pubbib id='havelund-rosu-2002-tacas' template='PubDefaultWithAbstractAndTitle'/> |

## Latest revision as of 14:37, 21 February 2016

## [edit] Journal of STTT

**Efficient Monitoring of Safety Properties**- Klaus Havelund and Grigore Rosu
, Volume 6(2), pp 158-173. 2004**J. of STTT**

*Abstract.*The problem of testing whether a finite execution trace of events generated by an executing program violates a linear temporal logic (LTL) formula occurs naturally in runtime analysis of software. Two efficient algorithms for this problem are presented in this paper, both for checking safety formulae of the form "always P", where P is a past time LTL formula. The first algorithm is implemented by rewriting and the second synthesizes efficient code from formulae. Further optimizations of the second algorithm are suggested, reducing space and time consumption. Special operators suitable for writing succinct specifications are discussed and shown equivalent to the standard past time operators. This work is part of NASA's PathExplorer project, the objective of which is to construct a flexible framework for efficient monitoring and analysis of program executions.

## [edit] TACAS'02

**Synthesizing Monitors for Safety Properties**- Klaus Havelund and Grigore Rosu
, LNCS 2280, pp 342-356. 2002**TACAS'02**

*Abstract.*The problem of testing a linear temporal logic (LTL) formula on a finite execution trace of events, generated by an executing program, occurs naturally in runtime analysis of software. An algorithm which takes a past time LTL formula and generates an efficient dynamic programming algorithm is presented. The generated algorithm tests whether the formula is satisfied by a finite trace of events given as input and runs in linear time, its constant depending on the size of the LTL formula. The memory needed is constant, also depending on the size of the formula. Further optimizations of the algorithm are suggested. Past time operators suitable for writing succinct specifications are introduced and shown definitionally equivalent to the standard operators. This work is part of the PathExplorer project, the objective of which it is to construct a flexible framework for monitoring and analyzing program executions.