Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Runtime Verification of C Programs
verfasst von : Klaus Havelund
Erschienen in: Testing of Software and Communicating Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present in this paper a framework,
Rmor
, for monitoring the execution of C programs against state machines, expressed in a textual (non-graphical) format in files separate from the program. The state machine language has been inspired by a graphical state machine language
Rmor
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.