Robust online monitoring of signal temporal logic

Signal temporal logic (STL) is a formalism used to rigorously specify requirements of cyberphysical systems (CPS), i.e., systems mixing digital or discrete components in interaction with a continuous environment or analog components. STL is naturally equipped with a quantitative semantics which can...

Full description

Saved in:
Bibliographic Details
Published in:Formal methods in system design 2017-08, Vol.51 (1), p.5-30
Main Authors: Deshmukh, Jyotirmoy V., Donzé, Alexandre, Ghosh, Shromona, Jin, Xiaoqing, Juniwal, Garvit, Seshia, Sanjit A.
Format: Article
Language:English
Subjects:
Automotive parts
Boolean algebra
CAE) and Design
CAI
Circuits and Systems
Computer assisted instruction
Computer simulation
Computer-Aided Engineering (CAD
Cyber-physical systems
Distance learning
Electrical Engineering
Engineering
Environmental monitoring
Semantics
Signal monitoring
Software Engineering/Programming and Operating Systems
Temporal logic
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Signal temporal logic (STL) is a formalism used to rigorously specify requirements of cyberphysical systems (CPS), i.e., systems mixing digital or discrete components in interaction with a continuous environment or analog components. STL is naturally equipped with a quantitative semantics which can be used for various purposes: from assessing the robustness of a specification to guiding searches over the input and parameter space with the goal of falsifying the given property over system behaviors. Algorithms have been proposed and implemented for offline computation of such quantitative semantics, but only few methods exist for an online setting, where one would want to monitor the satisfaction of a formula during simulation. In this paper, we formalize a semantics for robust online monitoring of partial traces, i.e., traces for which there might not be enough data to decide the Boolean satisfaction (and to compute its quantitative counterpart). We propose an efficient algorithm to compute it and demonstrate its usage on two large scale real-world case studies coming from the automotive domain and from CPS education in a Massively Open Online Course setting. We show that savings in computationally expensive simulations far outweigh any overheads incurred by an online approach.
ISSN:0925-9856
1572-8102
DOI:10.1007/s10703-017-0286-7