NASA Jet Propulsion Laboratory California Institute of Technology Follow this link to skip to the main content

BEACON eSpace at Jet Propulsion Laboratory >
JPL Technical Report Server >
JPL TRS 1992+ >

Please use this identifier to cite or link to this item:

Title: Runtime Verification of C Programs
Authors: Havelund, Klaus
Keywords: RMOR
machine language
RCAT (Requirement CApture Tool)
Issue Date: 10-Jan-2008
Publisher: Pasadena, CA : Jet Propulsion Laboratory, National Aeronautics and Space Administration, 2008
Citation: TESTCOM/FATES, Tokyo, Japan, June 10, 2008
Abstract: We present in this paper a framework, RMOR, for monitoring the execution of C programs against state machines, expressed in a textual (nongraphical) format in files separate from the program. The state machine language has been inspired by a graphical state machine language RCAT recently developed at the Jet Propulsion Laboratory, as an alternative to using Linear Temporal Logic (LTL) for requirements capture. Transitions between states are labeled with abstract event names and Boolean expressions over such. The abstract events are connected to code fragments using an aspect-oriented pointcut language similar to ASPECTJ’s or ASPECTC’s pointcut language. The system is implemented in the C analysis and transformation package CIL, and is programmed in OCAML, the implementation language of CIL. The work is closely related to the notion of stateful aspects within aspect-oriented programming, where pointcut languages are extended with temporal assertions over the execution trace.
Appears in Collections:JPL TRS 1992+

Files in This Item:

File Description SizeFormat
08-1083.pdf151.66 kBAdobe PDFView/Open

Items in DSpace are protected by copyright, but are furnished with U.S. government purpose use rights.


Privacy/Copyright Image Policy Beacon Home Contact Us
NASA Home Page + Div 27
+ JPL Space
Site last updated on December 5, 2014.
If you have any comments or suggestions for this web site, please e-mail Robert Powers.