Signal-Based Temporal Properties for Cyber-Physical Systems: Specification, Monitoring, and Diagnostics

Run-time verification (RV) is an analysis technique that focuses on observing the execution of a system to check its expected behavior against some specification. It is used for software verification and validation activities, such as operationalizing test oracles and defining run-time monitors.

The three main components of an effective RV approach are: i) a specification language allowing users to formally express the system requirements to be checked; ii) a monitoring algorithm that checks a system execution trace against the property specifications and yields a verdict indicating whether the input traces satisfies the property being checked; iii) a diagnostics algorithm that explains the cause of a requirement violation, in case of a negative verdict.

In this talk, I will review these three aspects taking into account the perspective of signal-based temporal properties for cyber-physical systems and will report on the application of the proposed formal methods in the context of collaborative research projects with industrial partners.