| タイトル | EAGLE Monitors by Collecting Facts and Generating Obligations |
| 本文（外部サイト） | http://hdl.handle.net/2060/20040010355 |
| 著者（英） | Havelund, Klaus; Sen, Koushik; Goldberg, Allen; Barrnger, Howard |
| 著者所属（英） | NASA Ames Research Center |
| 発行日 | 2003-01-01 |
| 言語 | eng |
| 内容記述 | 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. |
| NASA分類 | Computer Programming and Software |
| 権利 | Copyright, Distribution as joint owner in the copyright |
| URI | https://repository.exst.jaxa.jp/dspace/handle/a-is/222759 |
|
