HomePublicationsPaper

Work-In-Progress: a DSL for the safe deployment of Runtime Monitors in Cyber-Physical Systems
Ref: CISTER-TR-201002       Publication Date: 1 to 4, Dec, 2020

Abstract:
Guaranteeing that safety-critical Cyber-Physical Systems (CPS) do not fail upon deployment is becoming an even more complicated task with the increased use of complex software solutions. To aid in this matter, formal methods (rigorous mathematical and logical techniques) can be used to obtain proofs about the correctness of CPS in such a way that traditional testing methods cannot. Among the most promising formal methods is the concept of Runtime Verification, where monitors are coupled to a target system to check its behavior during runtime. Although helpful, runtime verification solutions introduce an inevitable overhead in the system, which can disrupt its correct functioning if not safely employed. We propose the creation of a Domain Specific Language (DSL) that, given a generic CPS, 1) verifies if its real-time scheduling is guaranteed, even in the presence of coupled monitors, and 2) implements several verification conditions for the correct-by-construction generation of monitoring architectures. To achieve it, we plan to perform statical verifications, derived from the available literature on schedulability analysis, and powered by a set of semi-automatic formal verification tools.

Giann Nandi

,

David Pereira

,

José Proença

,

Eduardo Tovar

Document:

View
PDF Download
PDF

Additional Files:

PDF
Poster