Abstract
Requirements of cyberphysical systems (CPS) can be rigorously specified using Signal Temporal Logic (STL). STL comes equipped with semantics that are able to quantify how robustly a given signal satisfies an STL property. In a setting where signal values over the entire time horizon of interest are available, efficient algorithms for offline computation of the robust satisfaction value have been proposed. Only a few methods exist for the online setting, i.e., where only a partial signal trace is available and rest of the signal becomes available in increments (such as in a real system or during numerical simulations). In this paper, we formalize the semantics for robust online monitoring of partial signals using the notion of robust satisfaction intervals (\(\mathtt {RoSI}\)s). We propose an efficient algorithm to compute the \(\mathtt {RoSI}\) and demonstrate its usage on two real-world case studies from the automotive domain and massively-online CPS education. As online algorithms permit early termination when the satisfaction or violation of a property is found, we show that savings in computationally expensive simulations far outweigh any overheads incurred by the online approach.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We omit the case of \(\mathbf {U}_I\) here for lack of space, although the rewriting approach of [7] can be adapted here and is implemented in our tool.
- 2.
We remark that \(\varphi \) is equivalent to \(\Box _{[0,a]} \left( (y > 0) \implies \Diamond _{[b,c]}(x>0)\right) \), which is a common formula used to express a timed causal relation between two signals.
References
Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011)
Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587, 3–25 (2015)
Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 23–37. Springer, Heidelberg (2014)
Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust Online Monitoring of Signal Temporal Logic (2015). arXiv pre-print
Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231–246. Springer, Heidelberg (2014)
Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)
Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264–279. Springer, Heidelberg (2013)
Donzé, A., Juniwal, G., Jensen, J.C., Seshia, S.A.: CPSGrader website. http://www.cpsgrader.org
Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010)
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)
Fainekos, G., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: Proceedings of the American Control Conference (2012)
Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)
Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178–192. Springer, Heidelberg (2014)
Hoxha, B., Abbas, H., Fainekos, G.: Benchmarks for temporal logic requirements for automotive systems. In: Proceedings of Applied Verification for Continuous and Hybrid Systems (2014)
Jin, X., Donzé, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: Proceedings of Hybrid Systems: Computation and Control, pp. 43–52 (2013)
Jones, A., Kong, Z., Belta, C.: Anomaly detection in cyber-physical systems: a formal methods approach. In: Proceedings of IEEE Conference on Decision and Control, pp. 848–853 (2014)
Juniwal, G., Donzé, A., Jensen, J.C., Seshia, S.A.: CPSGrader: synthesizing temporal logic testers for auto-grading an embedded systems laboratory. In: Proceedings of Conference on Embedded Software, October 2014
Kong, Z., Jones, A., Medina Ayala, A., Aydin Gol, E., Belta, C.: Temporal logic inference for classification and prediction from data. In: Proceedings of Hybrid Systems: Computation and Control, pp. 273–282 (2014)
Lemire, D.: Streaming Maximum-Minimum Filter Using no More Than Three Comparisons per Element (2006). arXiv preprint cs/0610046
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)
Nickovic, D., Maler, O.: AMT: a property-based monitoring tool for analog systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304–319. Springer, Heidelberg (2007)
Acknowledgments
This work was supported in part by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA, by NSF Expeditions grant CCF-1139138, and by Toyota under the CHESS center at UC Berkeley.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A. (2015). Robust Online Monitoring of Signal Temporal Logic. In: Bartocci, E., Majumdar, R. (eds) Runtime Verification. Lecture Notes in Computer Science(), vol 9333. Springer, Cham. https://doi.org/10.1007/978-3-319-23820-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-23820-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23819-7
Online ISBN: 978-3-319-23820-3
eBook Packages: Computer ScienceComputer Science (R0)