NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
EAGLE Monitors by Collecting Facts and Generating ObligationsWe present a rule-based framework, called EAGLE, that has been shown to be capable of defining and implementing a range of finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time and metric temporal logics, interval logics, forms of quantified temporal logics, and so on. A monitor for an EAGLE formula checks if a finite trace of states satisfies the given formula. We present, in details, an algorithm for the synthesis of monitors for EAGLE. The algorithm is implemented as a Java application and involves novel techniques for rule definition, manipulation and execution. Monitoring is achieved on a state-by-state basis avoiding any need to store the input trace of states. Our initial experiments have been successful as EAGLE detected a previously unknown bug while testing a planetary rover controller.
Document ID
20040010355
Acquisition Source
Ames Research Center
Document Type
Preprint (Draft being sent to journal)
Authors
Barrnger, Howard
(Manchester Univ. United Kingdom)
Goldberg, Allen
(Kestrel Technology, LLC Palo Alto, CA, United States)
Havelund, Klaus
(Kestrel Technology, LLC Palo Alto, CA, United States)
Sen, Koushik
(NASA Ames Research Center Moffett Field, CA, United States)
Date Acquired
September 7, 2013
Publication Date
January 1, 2003
Subject Category
Computer Programming And Software
Meeting Information
Meeting: TACAS ''04
Location: Barcelona
Country: Spain
Start Date: April 1, 2004
Funding Number(s)
CONTRACT_GRANT: EPSRC-GR/S40435/01
Distribution Limits
Public
Copyright
Public Use Permitted.
No Preview Available