REVERT: Runtime Verification for Real-Time Systems
Ref: CISTER-TR-161006 Publication Date: 29, Nov to 2, Dec, 2016
REVERT: Runtime Verification for Real-Time Systems
Ref: CISTER-TR-161006 Publication Date: 29, Nov to 2, Dec, 2016Abstract:
Real-time systems are becoming more complex and
open, thus increasing their development and verification costs.
Although several static verification tools have been proposed
over the last decades, they suffer from scalability and precision
problems. As a result, the tools fail to cover all the necessary
safety properties for realistic real-time applications involving a
large number of components and tasks. Runtime verification is a
formal technique that verifies properties during system execution
with the support of monitors. The monitors are generated
from formal languages using correct-by-construction generation
methods. Runtime verification can thus be used as a complement
or replacement for static verification approaches. The current
state-of-the-art tools either do not have notion of time, or suffer
from the potential blowup of states at run-time. In this paper,
we propose REVERT, a framework developed with a focus on
the verification of functional and non-functional properties with
timing constraints. The contribution of this work is twofold: (i) a
domain-specific specification language allowing the definition of
requirements for real-time applications; (ii) a novel mechanism to
generate monitors, with state-space and time guarantees, capable
of identifying and reacting to timing properties defined with the
proposed specification language.
Sangeeth Kochanthara
Geoffrey Nelissen
David PereiraDocument:
View
DownloadAdditional Files:
IEEE Real-Time Systems Symposium (RTSS 2016), WiP.
Porto, Portugal.
Record Date: 26, Oct, 2016