Skip to main content
SpringerLink
Log in

Monitoring and Measuring Hybrid Behaviors

A Tutorial

  • Conference paper
  • First Online:
Runtime Verification

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9333))

  • 1066 Accesses

Abstract

Continuous and hybrid behaviors naturally arise from many dynamical systems. In this tutorial, we present state-of-the-art techniques for qualitative and quantitative reasoning about such behaviors. We introduce Signal Temporal Logic and Timed Regular Expressions as specification languages that we use to describe properties of hybrid systems. We then provide an overview of methods for (1) checking whether a hybrid behavior is correct and robust with respect to its specification; and (2) measuring of quantitative characteristics of a hybrid system by property-driven extraction of relevant data from its behaviors. We present the tools that support such analysis and discuss their application in several application domains.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    To simplify the discussion about strictness of temporal operators, we restrict ourselves to the future fragment of the logics. The same argument applies for their past fragments.

  2. 2.

    The strictness of its temporal operators “forces” the time to advance.

  3. 3.

    We use multiset semantics as several patterns may have exactly the same measured value, in which case set semantics would not record its number of occurrences.

  4. 4.

    Computing STFT of a signal requires choosing a window function - TFL leaves the possibility of choosing different window functions.

References

  1. Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 356–374. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  2. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Asarin, E., Caspi, P., Maler, O.: A Kleene theorem for timed automata. In: Logic in Computer Science (LICS), pp. 160–171 (1997)

    Google Scholar 

  5. Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  6. Eugene Asarin, Alexandre Donzé, Oded Maler, and Dejan Nickovic. Parametric identification of temporal properties. In Runtime Verification - Second International Conference, RV 2011, San Francisco, CA, USA, September 27–30, 2011, Revised Selected Papers, pages 147–160 (2011)

    Google Scholar 

  7. Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 164–177. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. 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)

    Article  MathSciNet  MATH  Google Scholar 

  9. 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)

    Google Scholar 

  10. Brim, L., Dluhos, P., Safránek, D., Vejpustek, T.: \(\text{ STL }^*\): extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52–67 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  11. Brim, L., Vejpustek, T., Safránek, D., Fabriková, J.: Robustness analysis for value-freezing signal temporal logic. In: Proceedings Second International Workshop on Hybrid Systems and Biology, HSB 2013, Taormina, Italy, 2nd September 2013, pp. 20–36 (2013)

    Google Scholar 

  12. Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 391–403. Springer, Heidelberg (2014)

    Google Scholar 

  13. Chakarov, A., Sankaranarayanan, S., Fainekos, G.E.: Combining time and frequency domain specifications for periodic signals. In: Runtime Verification - Second International Conference, RV 2011, San Francisco, CA, USA, September 27–30, 2011, Revised Selected Papers, pp. 294–309 (2011)

    Google Scholar 

  14. Deshmukh, J.V., Majumdar, R., Prabhu, V.S.: Quantifying conformance using the skorokhod metric. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 234–250. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  15. Dluhos, P., Brim, L., Safránek, D.: On expressing and monitoring oscillatory dynamics. In: Proceedings First International Workshop on Hybrid Systems and Biology, HSB 2012, Newcastle Upon Tyne, UK, 3rd September 2012, pp. 73–87 (2012)

    Google Scholar 

  16. 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)

    Google Scholar 

  17. Donzé, A., Fanchon, E., Gattepaille, L.M., Maler, O., Tracqui, P.: Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE 6(9), e24246 (2011)

    Article  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 92–106. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  22. Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127–142. Springer, Heidelberg (2015)

    Google Scholar 

  23. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  24. Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In American Control Conference, ACC 2012, Montreal, QC, Canada, June 27–29, 2012, pp. 3567–3572 (2012)

    Google Scholar 

  25. Ferrère, T., Maler, O., Ničković, D., Ulus, D.: Measuring with timed patterns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 322–337. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  26. Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15–17, pp. 108–113 (2014)

    Google Scholar 

  27. Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.: SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, April 14–16, pp. 189–198 (2015)

    Google Scholar 

  28. Hoxha, B., Bach, H., Abbas, H., Dokhanci, A., Kobayashi, Y., Fainekos, G.: Towards formal specification visualization for testing and monitoring of cyber-physical systems. In: International Workshop on Design and Implementation of Formal Tools and Systems, DIFTS 2014 (2014)

    Google Scholar 

  29. Distributed System Interface. DSI3 Bus Standard. DSI Consortium

    Google Scholar 

  30. Juniwal, G., Donzé, A., Jensen, J.C., Seshia, S.A.: CPSGrader: Synthesizing temporal logic testers for auto-grading an embedded systems laboratory. In: 2014 International Conference on Embedded Software, EMSOFT 2014, New Delhi, India, October 12–17, 2014, pp. 24:1–24:10 (2014)

    Google Scholar 

  31. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  32. Majumdar, R., Prabhu, V.S.: Computing the Skorokhod distance between polygonal traces. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, April 14–16, 2015, pp. 199–208 (2015)

    Google Scholar 

  33. 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)

    Chapter  Google Scholar 

  34. Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247–268 (2013)

    Article  Google Scholar 

  35. Mobilia, N., Donzé, A., Moulis, J.M., Fanchon, E.: Producing a set of models for the iron homeostasis network. In: Proceedings Second International Workshop on Hybrid Systems and Biology, HSB 2013, Taormina, Italy, 2nd September 2013, pp. 92–98 (2013)

    Google Scholar 

  36. Nguyen, T., Ničković, D.: Assertion-based monitoring in practice – checking correctness of an automotive sensor interface. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 16–32. Springer, Heidelberg (2014)

    Google Scholar 

  37. Nickovic, D., Maler, O.: AMT: a property-based monitoring tool for analog systems. In: Proceedings of the Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3–5, 2007, pp. 304–319 (2007)

    Google Scholar 

  38. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 46–57 (1977)

    Google Scholar 

  39. Raman, V., Donzé, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, April 14–16, 2015, pp. 239–248 (2015)

    Google Scholar 

  40. Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 251–268. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  41. Sankaranarayanan, S., Miller, C., Raghunathan, R., Ravanbakhsh, H., Fainekos, G.E.: A model-based approach to synthesizing insulin infusion pump usage parameters for diabetic patients. In: 2012 50th Annual Allerton Conference on Communication, Control, and Computing, Allerton Park & Retreat Center, Monticello, IL, USA, October 1–5, 2012, pp. 1610–1617 (2012)

    Google Scholar 

  42. Stoma, S., Donzé, A., Bertaux, F., Maler, O., Batt, G.: STL-based analysis of TRAIL-induced apoptosis challenges the notion of type I/type II cell line classification. PLoS Comput. Bio. 9(5), e1003056 (2013)

    Article  Google Scholar 

  43. Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 222–236. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Acknowledgements

This work was supported by the MISTRAL project A-1341-RT-GP coordinated by the European Defence Agency (EDA) and funded by 8 contributing Members (France, Germany, Italy, Poland, Austria, Sweden, Netherland and Luxenbourg) in the framework of the Joint Investment Programme on Second Innovative Concepts and Emerging Technologies (JIP-ICET 2) and the IKT der Zukunft of Austrian FFG project HARMONIA (nr. 845631).

We are grateful to Oded Maler for his comments on the earlier drafts of this tutorial.

Author information

Authors and Affiliations

  1. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

Authors
  1. Dejan Ničković
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dejan Ničković .

Editor information

Editors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci

  2. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Ničković, D. (2015). Monitoring and Measuring Hybrid Behaviors. 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_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23820-3_26

  • 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)

Publish with us

Policies and ethics

Search

Navigation