Run time monitoring of reactive system models
MetadataShow full item record
In model-based development of reactive systems, statecharts are widely used for formal design of system behavior, and provide a sound basis for analysis and verification tools, as well as for code generation from system models. We present an approach for dynamic analysis of reactive systems via run-time verification of code produced with Statemate C and MicroC code generators , . The core of the approach is automatic creation of monitoring statecharts from formulas that specifiy the system's behavioral properties in a proposed assertion language. Such monitors are then translated into code together with the system model, and executed concurrently with the system code. This approach leads to a more realistic analysis of reactive systems, as monitoring is supported in the system's actual operating environment. For models that include design-level attributes (division into tasks, etc.), this is crucial for performance-related checks, and help to overcome restrictions inherent in simulation and model checking.
Showing items related by title, author, creator and subject.
Auguston, Mikhail; Trakhtenbrot, Mark (2008);In model-driven development of reactive systems, statecharts are widely used for formal description of their behavior, providing a sound basis for verification, testing and code generation. The paper presents an approach ...
Drusinsky, Doron; Shing, Man-Tak (2003);Run-time monitoring of temporal properties and assertions is used for testing and as a component of execution-based model checking techniques. Traditional run-time monitoring however, is limited to observing sequences ...
Ahart, Jennifer L. (Monterey, California. Naval Postgraduate School, 2007-06);The purpose of this thesis is to estimate the potential performance improvement in sustaining engineering (SE) when an Open Architecture (OA) approach to system development is used. Its basis is that in Integrated Warfare ...