EAGLE Monitors by Collecting Facts and Generating Obligations
- Author:
- Havelund, Klaus
- Published:
- [2003].
- Physical Description:
- 1 electronic document
- Additional Creators:
- Sen, Koushik, Goldberg, Allen, and Barrnger, Howard
Online Version
- hdl.handle.net , Connect to this object online.
- Restrictions on Access:
- Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access - Summary:
- We 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.
- Other Subject(s):
- Collection:
- NASA Technical Reports Server (NTRS) Collection.
- Note:
- Document ID: 20040010355.
TACAS '04; Apr. 2004; Barcelona; Spain. - Terms of Use and Reproduction:
- Copyright, Distribution as joint owner in the copyright.
View MARC record | catkey: 15966038