|
BEACON eSpace at Jet Propulsion Laboratory >
JPL Technical Report Server >
JPL TRS 1992+ >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/2014/41738
|
| 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. |
| URI: | http://hdl.handle.net/2014/41738 |
| Appears in Collections: | JPL TRS 1992+
|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
|
