RML: Runtime Monitoring Language, a System-Agnostic DSL for Runtime Verification
Runtime verification (RV) is a formal software verification technique in which a single execution of the software under scrutiny is checked at runtime, rather than statically verify the whole program. This is usually implemented through an instrumentation layer observing the system execution, and a monitor verifying the correctness of observed events. RML is a domain specific language expressly devised for specification writing in the context of RV: it is a high-level formalism with a rich set of operators and a programmer-friendly syntax. RML is completely system-agnostic, making it suitable for RV of virtually any kind of system. This is possible thanks to the proposed infrastructure in which the monitor (automatically synthesized from the specification) is decoupled from the instrumentation.
Fri 19 JulDisplayed time zone: Belfast change
10:30 - 12:10
|Invited talk: Runtime Verification and Objects: Are we doing it wrong?
Giles Reger University of Manchester
|Efficient Run-time Method for Detecting and Resolving Deadlocks in Java Programs
P: Eman Aldakheel University of Illinois at Chicago & Princess Nourah bint Abdulrahman University, Ugo BuyPre-print
|RML: Runtime Monitoring Language, a System-Agnostic DSL for Runtime Verification
P: Luca Franceschini DIBRIS, University of Genova, ItalyPre-print