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

fYear

2001

fDate

26-29 Nov. 2001

Firstpage

412

Lastpage

416

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on

ISSN

1938-4300

Print_ISBN

0-7695-1426-X

Type

conf

DOI

10.1109/ASE.2001.989841

Filename

989841