Cyber-physical systems (CPS) integrate heterogeneous collaborative components that are interconnected between themselves and their physical environment. They exhibit complex behaviors that typically combine discrete and continuous dynamics.
The tremendous complexity of the CPS applications, such as autonomous vehicles, makes full and exhaustive verification of the system during design-time virtually impossible. Runtime verification addresses this problem by providing a formal, yet scalable, verification and analysis method.
Runtime verification can be applied to:
- Real systems during their execution
- System model during design phase, where behaviors correspond to simulation traces
In the first case, runtime verification is used to detect potential system deviations from the nominal behavior and possibly take corrective actions. In the second case, runtime verification is used to complement formal verification methods by enabling rigorous analysis of the individual system behaviors.
In DSE, we address three major topics related to the runtime verification of CPS:
- Specification languages for expressing common CPS properties
- Novel runtime verification and analysis techniques
- Fault explanation and localization
In particular, we currently focus on the following specific aspects:
- Development and deployment of real-time monitors
- Predictive system health monitoring
- Property-driven parameter extraction and measurements from behaviors
- Trace and system diagnosis
- Correctness vs. robustness runtime verification
