Run-Time Checking of Dynamic Properties

We consider a first-order property specification language for run-time monitoring of dynamic systems. The language is based on a linear-time temporal logic and offers two kinds of quantifiers to bind free variables in a formula. One kind contains the usual first-order quantifiers that provide for re...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2006-05, Vol.144 (4), p.91-108
Main Authors: Sokolsky, Oleg, Sammapun, Usa, Lee, Insup, Kim, Jesung
Format: Article
Language:English
Subjects:
linear-time temporal logic
run-time monitoring
Specification language
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We consider a first-order property specification language for run-time monitoring of dynamic systems. The language is based on a linear-time temporal logic and offers two kinds of quantifiers to bind free variables in a formula. One kind contains the usual first-order quantifiers that provide for replication of properties for dynamically created and destroyed objects in the system. The other kind, called attribute quantifiers, is used to check dynamically changing values within the same object. We show that expressions in this language can be efficiently checked over an execution trace of a system.
ISSN:1571-0661
1571-0661
DOI:10.1016/j.entcs.2006.02.006