Back to Search
Start Over
RML: Theory and practice of a domain specific language for runtime verification
- Source :
- Science of Computer Programming. 205:102610
- Publication Year :
- 2021
- Publisher :
- Elsevier BV, 2021.
-
Abstract
- Runtime verification (RV) is an approach to verification consisting in dynamically checking that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected correct behavior. RML (Runtime Monitoring Language) is a simple but powerful Domain Specific Language (DSL) for RV which is able to express non context-free properties. When designing RML, particular care has been taken to favor abstraction and simplicity, to better support reusability and portability of specifications and interoperability of the monitors generated from them; this is mainly achieved by decoupling the two problems of property specification and event generation, and by minimizing the available primitive constructs. The formalization and implementation of RML is based on a trace calculus with a fully deterministic rewriting semantics. The semantics of RML is defined by translation into such a calculus, which, in fact, is used as intermediate representation (IR) by the RML compiler. The effectiveness of RML and its methodological impact on RV are presented through interesting patterns that can be adapted to different contexts requiring verification of standard properties. A collection of tested examples is provided, together with benchmarks showing that the deterministic semantics and the performed dynamic optimizations based on the laws of the trace calculus significantly improve the performances of the generated monitors.
- Subjects :
- Domain-specific language
Semantics (computer science)
Computer science
Programming language
Runtime verification
020207 software engineering
02 engineering and technology
Runtime verification, Domain specific language, Operational semantics
Domain specific language
computer.software_genre
Software portability
020204 information systems
Formal specification
Operational semantics
0202 electrical engineering, electronic engineering, information engineering
Compiler
Rewriting
computer
Software
TRACE (psycholinguistics)
Subjects
Details
- ISSN :
- 01676423
- Volume :
- 205
- Database :
- OpenAIRE
- Journal :
- Science of Computer Programming
- Accession number :
- edsair.doi.dedup.....db4e305c7444d5a977f05b10e16c24aa