NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Runtime Analysis of Linear Temporal Logic SpecificationsThis report presents an approach to checking a running program against its 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 B chi 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.
Document ID
20030063271
Acquisition Source
Langley Research Center
Document Type
Other
Authors
Giannakopoulou, Dimitra
(Research Inst. for Advanced Computer Science Moffett Field, CA, United States)
Havelund, Klaus
(Research Inst. for Advanced Computer Science Moffett Field, CA, United States)
Date Acquired
August 21, 2013
Publication Date
August 1, 2001
Subject Category
Computer Programming And Software
Report/Patent Number
RIACS-TR-01.21
Meeting Information
Meeting: 16th IEEE International Conference on Automated Software Engineering
Location: San Diego, CA
Country: United States
Start Date: January 1, 2001
Sponsors: Institute of Electrical and Electronics Engineers
Funding Number(s)
CONTRACT_GRANT: NCC2-1006
Distribution Limits
Public
Copyright
Public Use Permitted.
Document Inquiry

Available Downloads

There are no available downloads for this record.
No Preview Available