EvTL: A Temporal Logic for the Transient Analysis of Cyber-Physical Systems

TL;DR

This paper introduces EvTL, a stochastic temporal logic for specifying and verifying the transient behavior of cyber-physical systems under uncertainty, with a robustness semantics and a statistical model checking approach.

Contribution

The paper presents EvTL, a novel stochastic extension of STL, with a sound and complete semantics and a statistical model checking algorithm for system verification.

Findings

EvTL effectively captures probabilistic transient behaviors.

The framework is validated through a three-tanks laboratory experiment.

EvTL provides robustness measures for system requirements.

Abstract

The behaviour of systems characterised by a closed interaction of software components with the environment is inevitably subject to perturbations and uncertainties. In this paper we propose a general framework for the specification and verification of requirements on the behaviour of these systems. We introduce the Evolution Temporal Logic (EvTL), a stochastic extension of STL allowing us to specify properties of the probability distributions describing the transient behaviour of systems, and to include the presence of uncertainties in the specification. We equip EvTL with a robustness semantics and we prove it sound and complete with respect to the semantics induced by the evolution metric, i.e., a hemimetric expressing how well a system is fulfilling its tasks with respect to another one. Finally, we develop a statistical model checking algorithm for EvTL specifications. As an example of an application of our framework, we consider a three-tanks laboratory experiment.