×

Quantitative monitoring of STL with edit distance. (English) Zbl 1394.68230

Summary: In cyber-physical systems (CPS), physical behaviors are typically controlled by digital hardware. As a consequence, continuous behaviors are discretized by sampling and quantization prior to their processing. Quantifying the similarity between CPS behaviors and their specification is an important ingredient in evaluating correctness and quality of such systems. We propose a novel procedure for measuring robustness between digitized CPS signals and signal temporal logic (STL) specifications. We first equip STL with quantitative semantics based on the weighted edit distance, a metric that quantifies both space and time mismatches between digitized CPS behaviors. We then develop a dynamic programming algorithm for computing the robustness degree between digitized signals and STL specifications. In order to promote hardware-based monitors we implemented our approach in FPGA. We evaluated it on automotive benchmarks defined by research community, and also on realistic data obtained from magnetic sensor used in modern cars.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

S-TaLiRo; Breach; ANTLR
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abbas H, Mittelmann HD, Fainekos GE (2014) Formal property verification in a conformance testing framework. In: Proceedings of MEMOCODE 2014: the twelfth ACM/IEEE international conference on formal methods and models for codesign, pp 155-164. IEEE. https://doi.org/10.1109/MEMCOD.2014.6961854
[2] Akazaki T, Tasuo I (2015) Time robustness in MTL and expressivity in hybrid system falsification. In: Proceedings of CAV 2015: the 27th international conference on computer aided verification, LNCS, vol 9207. Springer. https://doi.org/10.1007/978-3-319-21668-3 · Zbl 1381.68142
[3] Allauzen C, Mohri M (2009) Linear-space computation of the edit-distance between a string and a finite automaton. CoRR arXiv:0904.4686 · Zbl 1216.68350
[4] Annpureddy Y, Liu C, Fainekos GE, Sankaranarayanan S (2011) S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Proceedings of TACAS 2011: the 17th international conference on tools and algorithms for the construction and analysis of systems, LNCS, vol 6605, pp 254-257. Springer. https://doi.org/10.1007/978-3-642-19835-9_21 · Zbl 1316.68069
[5] Bardh Hoxha HA, Fainekos G (2015) Benchmarks for temporal logic requirements for automotive systems. In: Proceedings of ARCH@CPSWeek 2014 and ARCH@CPSWeek 2015: the 1st and 2nd international workshop on applied verification for continuous and hybrid systems, vol 34
[6] Bartocci E, Bortolussi L, Sanguinetti G (2014) Data-driven statistical learning of temporal logic properties. In: Proceedings of FORMATS 2014: the 12th international conference on formal modeling and analysis of timed systems, LNCS, vol 8711, pp 23-37. Springer. https://doi.org/10.1007/978-3-319-10512-3_3 · Zbl 1448.68371
[7] Brim, L; Dluhos, P; Safránek, D; Vejpustek, T, \({STL}^*\): extending signal temporal logic with signal-value freezing operator, Inf Comput, 236, 52-67, (2014) · Zbl 1311.68085 · doi:10.1016/j.ic.2014.01.012
[8] Davoren JM (2009) Epsilon-tubes and generalized Skorokhod metrics for hybrid paths spaces. In: Proceedings of HSCC 2009: the 12th international conference on hybrid systems: computation and control, LNCS, vol 5469, pp 135-149. Springer. https://doi.org/10.1007/978-3-642-00602-9_10 · Zbl 1237.93088
[9] Deshmukh, JV; Donzé, A; Ghosh, S; Jin, X; Juniwal, G; Seshia, SA, Robust online monitoring of signal temporal logic, Form Methods Syst Des, 51, 5-30, (2017) · Zbl 1370.68199 · doi:10.1007/s10703-017-0286-7
[10] Deshmukh JV, Majumdar R, Prabhu VS (2015) Quantifying conformance using the Skorokhod metric (full version). CoRR arXiv:1505.05832
[11] Deshmukh, JV; Majumdar, R; Prabhu, VS, Quantifying conformance using the Skorokhod metric, Form Methods Syst Des, 50, 168-206, (2017) · Zbl 1360.68629 · doi:10.1007/s10703-016-0261-8
[12] Dokhanchi A, Hoxha B, Fainekos GE (2014) On-line monitoring for temporal logic robustness. In: Proceedings RV 2014: the 5th international conference on runtime verification, LNCS, vol 8734, pp 231-246. Springer. https://doi.org/10.1007/978-3-319-11164-3_19
[13] Donzé A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proceedings of CAV 2010: the 22nd international conference on computer aided verification, LNCS, vol 6174, pp 167-170. Springer. https://doi.org/10.1007/978-3-642-14295-6_17
[14] Donzé A, Ferrère T, Maler O (2013) Efficient robust monitoring for STL. In: Proceedings of CAV 2013: the 25th international conference on computer aided verification, LNCS, vol 8044, pp 264-279. Springer. https://doi.org/10.1007/978-3-642-39799-8 · Zbl 1075.68611
[15] Donzé A, Maler O (2010) Robust satisfaction of temporal logic over real-valued signals. In: Proceedings of FORMATS 2010: the 8th international conference on formal modeling and analysis of timed systems, LNCS, vol 6246, pp 92-106. Springer. https://doi.org/10.1007/978-3-642-15297-9
[16] Droste M, Kuich W, Vogler H (2009) Handbook of weighted automata. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-01492-5 · Zbl 1200.68001
[17] Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: Proceedings of the computer aided verification, 15th international conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, pp 27-39 · Zbl 1278.68168
[18] Fainekos, GE; Pappas, GJ, Robustness of temporal logic specifications for continuous-time signals, Theor Comput Sci, 410, 4262-4291, (2009) · Zbl 1186.68287 · doi:10.1016/j.tcs.2009.06.021
[19] Fainekos GE, Sankaranarayanan S, Ivancic F, Gupta A (2009) Robustness of model-based simulations. In: Proceedings of RTSS 2009: the 30th IEEE real-time systems symposium, pp 345-354. IEEE Computer Society. https://doi.org/10.1109/RTSS.2009.26
[20] Gerth R, Peled D, Vardi MY, Wolper P (1996) Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the fifteenth IFIP WG6.1 international symposium on protocol specification, testing and verification, IFIP conference proceedings, vol 38, pp 3-18. Chapman & Hall
[21] Herrmann L, Vogler H (2016) Weighted symbolic automata with data storage. In: Proceedings of DLT 2016: the 20th international conference on developments in language theory, LNCS, vol 9840, pp 203-215. Springer. https://doi.org/10.1007/978-3-662-53132-7 · Zbl 1436.68172
[22] http://jautomata.sourceforge.net/. Accessed 28 March 2017
[23] http://www.mathworks.com/products/demos/stateflow/fuelsys.html. Accessed 28 March 2017
[24] International S (2016) SENT—single edge nibble transmission for automotive applications, J2716, Standard. http://standards.sae.org/j2716_201001/. Accessed 21 Jan 2017
[25] Jaksic S, Bartocci E, Grosu R, Nickovic D (2016) Quantitative monitoring of STL with edit distance. In: Proceedings of RV 2016: the 16th international conference on runtime verification, LNCS, vol 10012, pp 201-218. Springer. https://doi.org/10.1007/978-3-319-46982-9_13 · Zbl 1394.68230
[26] Konstantinidis, S, Computing the edit distance of a regular language, Inf Comput, 205, 1307-1316, (2007) · Zbl 1127.68053 · doi:10.1016/j.ic.2007.06.001
[27] Krause EF (2012) Taxicab geometry: an adventure in non-Euclidean geometry. Courier Corporation, North Chelmsford
[28] Levenshtein, VI, Binary codes capable of correcting deletions, insertions and reversals, Sov Phys Dokl, 10, 707, (1966)
[29] Maler, O; Nickovic, D, Monitoring properties of analog and mixed-signal circuits, STTT, 15, 247-268, (2013) · doi:10.1007/s10009-012-0247-9
[30] Mohri, M, Edit-distance of weighted automata: general definitions and algorithms, Int J Found Comput Sci, 14, 957-982, (2003) · Zbl 1075.68611 · doi:10.1142/S0129054103002114
[31] Nguyen T, Nickovic D (2014) Assertion-based monitoring in practice—checking correctness of an automotive sensor interface. In: Proceedings of FMICS 2014: the 19th international conference on formal methods for industrial critical systems, LNCS, vol 8718, pp 16-32. Springer. https://doi.org/10.1007/978-3-319-10702-8
[32] Parr T (2013) The definitive ANTLR 4 reference, 2nd edn. Pragmatic Bookshelf, Dallas
[33] Pnueli A, Zaks A (2008) On the merits of temporal testers. In: 25 years of model checking—history, achievements, perspectives, LNCS, vol 5000, pp 172-195. Springer. https://doi.org/10.1007/978-3-540-69850-0 · Zbl 1143.68046
[34] Quesel J (2013) Similarity, logic, and games—bridging modeling layers of hybrid systems. Ph.D. thesis, Universität Oldenburg · Zbl 1370.68199
[35] Rizk A, Batt G, Fages F, Soliman S (2008) On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Proceedings of CMSB 2008: the 6th international conference on computational methods in systems biology, LNCS, vol 5307, pp 251-268. Springer. https://doi.org/10.1007/978-3-540-88562-7
[36] Samanta R, Deshmukh JV, Chaudhuri S (2013) Robustness analysis of string transducers. In: Proceedings of ATVA 2013: the 11th international symposium on automated technology for verification and analysis, LNCS, vol 8172, pp 427-441. Springer. https://doi.org/10.1007/978-3-319-02444-8_30 · Zbl 1311.68085
[37] Schulz, UK; Mihov, S, Fast string correction with levenshtein automata, Int J Doc Anal Recognit, 5, 67-85, (2002) · Zbl 1039.68137 · doi:10.1007/s10032-002-0082-8
[38] Selyunin K, Jaksic S, Nguyen T, Reidl C, Hafner U, Bartocci E, Nickovic D, Grosu R (2017) Runtime monitoring with recovery of the SENT communication protocol. In: Proceedings of CAV 2017: the 29th international conference on computer aided verification, LNCS, vol 10426, pp 336-355. Springer. https://doi.org/10.1007/978-3-319-63387-9
[39] Skorokhod, AV, Limit theorems for stochastic processes, Theory Probab Appl, 1, 261-290, (1956) · Zbl 0074.33802 · doi:10.1137/1101022
[40] Unser, M, Sampling 50 years after Shannon, Proc IEEE, 88, 569-587, (2000) · doi:10.1109/5.843002
[41] Veanes M, Bjørner N, de Moura LM (2010) Symbolic automata constraint solving. In: Proceedings of LPAR-17: the 17th international conference on logic for programming, artificial intelligence, and reasoning, LNCS, vol 6397, pp 640-654. Springer. https://doi.org/10.1007/978-3-642-16242-8 · Zbl 1306.68097
[42] Wagner, RA, Order-n correction for regular languages, Commun ACM, 17, 265-268, (1974) · Zbl 0276.68011 · doi:10.1145/360980.360995
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.