Runtime Reflection
The runtime reflection project establishes methods to dynamically analyse reactive distributed systems at runtime. The approach is layered and modular in that we provide the means for first detecting failures of a system by means of runtime verification and secondly, provide means for identifying their causes by means of a detailed diagnosis. As such, diagnoses can be subsequently used in order to trigger recovery measures, or to store detailed log-files for off-line analysis.
In principle, runtime reflection spans from the early development phases, e.g., systems design and specification to their actual implementation and analysis at runtime; thus, ultimately at more fault-tolerant systems.
On this project page we provide the tools which make up our framework to accomplish the above objectives. In particular, we currently offer a tool for automatically generating so-called runtime monitors from a given LTL-specification which can be used to monitor arbitrary C++-programs. The tool allows to annotate C++-code in order to generate log-records for events such as function entries and exits, unexpected exceptions, violated assertions, and passing of simple trace points. The resulting traces of a program execution can then be analysed at runtime for erroneous behaviour by the generated monitor. The tool will report a violation of a given property immediately when it is clear that it will eventually happen.
Additionally, we provide an implementation to perform the main diagnostic task; that is, based on the results of the monitors, find causes for occurred errors. The implementation is currently based on a highly optimised SAT-solver, which computes for a number of given symptoms possible conflict sets, hence diagnoses, that explain the undesired behaviour. As such, we are able to differentiate between the symptoms of a fault, and the actual fault itself.
News
Jan-30-2006: Added documentation
In the documentation section, you can now find a number of papers which detail on the methods used in the runtime reflection framework.
Oct-25-2005: Released lsat_diagnosis 0.0.1 (development)
The diagnosis component is now publicly available from the downloads section. Its aim is to use the monitor results in order to identify causes of failure and thus, differntiate from mere symptoms of a failure. For now, please refer to the tar-ball for a detailed documentation of this component. Your feedback is more than welcome!
Oct-18-2005: Released runtime_verification 0.0.1 (development)
The first public release of the runtime verification framework has been released. It is available in the downloads section. Please, report feedback.
Documentation
Runtime reflection is part of a research initiative and its background documented in several publications, some of which are listed below.
- Simplifying Diagnosis Using LSAT: A Propositional Approach to Reasoning from First Principles. Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Second International Conference, CPAIOR 2005, Prague, Czech Republic, May 30 - June 1, 2005, Proceedings. Lecture Notes in Computer Science 3524 2005.
- Runtime verification revisited. Technical report TUM-I0518, Institut für Informatik, Technische Universität München. 2005.
- Model-based runtime analysis of distributed reactive systems. 17th Australian Software Engineering Conference {(ASWEC} 2006), 18-21 April 2006, Sydney, Australia. 2006.
Download
To download the latest versions of our components, simply click the links to the gzipped tar-balls below. Detailed instructions on how to compile, and install the framework are given inside the respective tar-balls.
Latest Version: 0.0.1
- Gzipped source archive of runtime_verification 0.0.1 (301 KBytes)
- Gzipped source archive of lsat_diagnosis 0.0.1 (1.1 MBytes)
Contact
If you have further questions feel free to contact Martin Leucker.