NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Runtime Verification of C ProgramsWe 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.
Document ID
20110013163
Document Type
Conference Paper
External Source(s)
Authors
Havelund, Klaus (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Date Acquired
August 25, 2013
Publication Date
January 10, 2008
Subject Category
Mathematical and Computer Sciences (General)
Meeting Information
TESTCOM/FATES(Tokyo)
Distribution Limits
Public
Copyright
Other
Keywords
RMOR
RCAT (Requirement CApture Tool)
machine language