Result: Efficient monitoring of safety properties

Title:
Efficient monitoring of safety properties
Authors:
HAVELUND, Klaus, ROSU, Grigore
Source:
International journal on software tools for technology transfer (Print). 6(2):158-173
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 37 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Exécution programme, Program execution, Ejecución programa, Logique linéaire, Linear logic, Lógica lineal, Logique temporelle, Temporal logic, Lógica temporal, Monitorage, Monitoring, Monitoreo, Programmation dynamique, Dynamic programming, Programación dinámica
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Kestrel Technology, NASA Ames Research Center, Moffett Field, CA, United States
Department of Computer Science, University of Illinois at Urbana-Champaign, United States
ISSN:
1433-2779
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=16328061
Rights:
Copyright 2005 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.16328061
Database:
PASCAL Archive

Further Information

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 to be 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.