Title :
Automata-based verification of temporal properties on running programs
Author :
Giannakopoulou, Dimitra ; Havelund, Klaus
Author_Institution :
Automated Software Eng. Group, NASA Ames Res. Center, CA, USA
Abstract :
This paper presents an approach to checking a running program against Linear Temporal Logic (LTL) specifications. LTL is a widely used logic for expressing properties of programs viewed as sets of executions. Our approach consists of translating LTL formulae to finite-state automata, which are used as observers of the program behavior. The translation algorithm we propose modifies standard LTL to Buchi automata conversion techniques to generate automata that check finite program traces. The algorithm has been implemented in a tool, which has been integrated with the generic JPaX framework for runtime analysis of Java programs.
Keywords :
finite automata; formal specification; program verification; temporal logic; Buchi automata conversion; Java programs; automata-based verification; finite state automata; generic JPaX framework; linear temporal logic specifications; observers; program behavior; running programs; runtime analysis; temporal properties; Algorithm design and analysis; Automata; Computer industry; Computerized monitoring; Java; Logic testing; NASA; Runtime; Software engineering; Space technology;
Conference_Titel :
Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on
Print_ISBN :
0-7695-1426-X
DOI :
10.1109/ASE.2001.989841
