Robust online monitoring of signal temporal logic. (English) Zbl 1370.68199
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.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68W27 | Online algorithms; streaming algorithms |
Keywords:
cyberphysical systems; runtime verification; online monitoring; signal temporal logic; quantitative semanticsReferences:
| [1] | Annpureddy Y, Liu C, Fainekos G, Sankaranarayanan S (2011) S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: TACAS. pp 254-257 · Zbl 1316.68069 |
| [2] | Bartocci E, Bortolussi L, Sanguinetti G (2014) Data-driven statistical learning of temporal logic properties. In: Formal modeling and analysis of timed systems. Springer International Publishing, pp 23-37 · Zbl 1448.68371 |
| [3] | Dokhanchi A, Hoxha B, Fainekos G (2014) On-line monitoring for temporal logic robustness. In: RV. pp 231-246 · Zbl 1186.68287 |
| [4] | Donzé A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: CAV. pp 167-170 |
| [5] | Donzé A, Ferrère T, Maler O (2013) Efficient robust monitoring for STL. In: CAV. pp 264-279 · Zbl 1186.68287 |
| [6] | Donzé A, Juniwal G, Jensen JC, Seshia SA, Cpsgrader website. http://www.cpsgrader.org |
| [7] | Donzé A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: Formal modeling and analysis of timed systems. pp 92-106 · Zbl 1290.68071 |
| [8] | Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: CAV. pp 27-39 · Zbl 1278.68168 |
| [9] | Fainekos G, Sankaranarayanan S, Ueda K, Yazarel H (2012) Verification of automotive control applications using s-taliro. In: Proceedings of the American Control Conference |
| [10] | Fainekos GE, Pappas GJ (2009) Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42):4262-4291 · Zbl 1186.68287 · doi:10.1016/j.tcs.2009.06.021 |
| [11] | Ho H-M, Ouaknine J, Worrell J (2014) Online monitoring of metric temporal logic. In: Runtime verification · Zbl 1515.68181 |
| [12] | Hoxha B, Abbas H, Fainekos G (2014) Benchmarks for temporal logic requirements for automotive systems. In: Proceedings of applied verification for continuous and hybrid systems |
| [13] | Jaksic S, Bartocci E, Grosu R, Kloibhofer R, Nguyen T, Nickovic D (2015) From signal temporal logic to FPGA monitors. In: 13. ACM/IEEE international conference on formal methods and models for codesign, MEMOCODE 2015, Austin, 21-23 Sept 2015. IEEE, pp 218-227 |
| [14] | Jin X, Deshmukh JV, Kapinski J, Ueda K, Butts K (2014) Powertrain control verification benchmark. In: Proceedings of hybrid systems: computation and control. pp 253-262 · Zbl 1362.93070 |
| [15] | Jin X, Donzé A, Deshmukh JV, Seshia SA (2013) Mining requirements from closed-loop control models. In: Proceedings of HSCC. pp 43-52 · Zbl 1362.93008 |
| [16] | Juniwal G, Donzé A, Jensen JC, Seshia SA (2014) CPSGrader: synthesizing temporal logic testers for auto-grading an embedded systems laboratory. In: EMSOFT |
| [17] | Kong Z, Jones A, Medina Ayala A, Aydin Gol E, Belta C (2014) Temporal logic inference for classification and prediction from data. In: Proceedings of the 17th international conference on hybrid systems: computation and control. ACM, pp 273-282 · Zbl 1362.68266 |
| [18] | Lemire D (2006) Streaming maximum-minimum filter using no more than three comparisons per element. arXiv preprint arXiv:cs/0610046 · Zbl 1123.68138 |
| [19] | Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: FORMATS/FTRTFT. pp 152-166 · Zbl 1109.68518 |
| [20] | MATLAB/Simulink (2015) Version R2015a. The MathWorks Inc., Natick |
| [21] | Nickovic D, Maler O (2007) AMT: A property-based monitoring tool for analog systems. Form Model Anal Timed Syst 4763:304-319 · doi:10.1007/978-3-540-75454-1_22 |
| [22] | Rodionova A, Bartocci E, Nickovic D, Grosu R (2016) Temporal logic as filtering. In: Abate A, Fainekos GE (eds) Proceedings of the 19th international conference on hybrid systems: computation and control, HSCC 2016, Vienna, 12-14 Apr 2016. ACM, pp 11-20 · Zbl 1364.94156 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
