Skip to main content
SpringerLink
Log in

Monitoring Temporal Properties of Continuous Signals

  • Conference paper
Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems (FTRTFT 2004, FORMATS 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3253))

Abstract

In this paper we introduce a variant of temporal logic tailored for specifying desired properties of continuous signals. The logic is based on a bounded subset of the real-time logic mitl, augmented with a static mapping from continuous domains into propositions. From formulae in this logic we create automatically property monitors that can check whether a given signal of bounded length and finite variability satisfies the property. A prototype implementation of this procedure was used to check properties of simulation traces generated by Matlab/Simulink.

This work was partially supported by the EC projects IST-2001-33520 CC (Control and Computation), IST-2001-35302 AMETIST (Advanced Methods for Timed Systems) and IST-2003-507219 PROSYD (Property-Based System Design).

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abarbanel, Y., Beer, I., Glushovsky, L., Keidar, S., Wolfsthal, Y.: FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 538–542. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Alur, R., Feder, T., Henzinger, T.A.: The Benefits of Relaxing Punctuality. Journal of the ACM 43(1), 116–146 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  3. Alur, R., Henzinger, T.A.: Logics and Models of Real-Time: A Survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  4. Beer, I., Ben David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 363. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)

    MATH  Google Scholar 

  6. Bensalem, S., Bozga, M., Krichen, M., Tripakis, S.: Testing Conformance of Real-time Applications with Automatic Generation of Observers. In: Proc. RV 2004 (2004) (to appear in ENTCS)

    Google Scholar 

  7. Bendotti, P.: Steam Generator Water Level Control Problem. Technical report, CC project (2002)

    Google Scholar 

  8. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  9. Donzé, A.: Etude d’un Modèle de Contrôleur Hybride. Master’s thesis, INPG (2003)

    Google Scholar 

  10. Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  12. Geilen, M.C.W., Dams, D.R.: An On-the-fly Tableau Construction for a Realtime Temporal Logic. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 276–290. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  13. Geilen, M.C.W.: Formal Techniques for Verification of Complex Real-time Systems. PhD thesis, Eindhoven University of Technology (2002)

    Google Scholar 

  14. Geilen, M.C.W.: An Improved On-the-fly Tableau Construction for a Real-time Temporal Logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 394–406. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  15. Henzinger, T.A.: It’s about Time: Real-time Logics Reviewed. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 439–454. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  16. Havelund, K., Rosu, G.: Java PathExplorer - a Runtime Verification Tool. In: Proc. ISAIRAS 2001 (2001)

    Google Scholar 

  17. Havelund, K., Rosu, G. (eds.): Runtime Verification RV 2002. ENTCS, vol. 70(4) (2002)

    Google Scholar 

  18. Havelund, K., Rosu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Kim, M., Lee, I., Sammapun, U., Shin, J., Sokolsky, O.: Monitoring, Checking, and Steering of Real-time Systems. In: Proc. RV 2002. ENTCS, vol. 70(4) (2002)

    Google Scholar 

  20. Kristoffersen, K.J., Pedersen, C., Andersen, H.R.: Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems. In: Proc. RV 2003. ENTCS, vol. 89(2) (2003)

    Google Scholar 

  21. Krichen, M., Tripakis, S.: Black-box Conformance Testing for Real-time Systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 109–126. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  22. Kurshan, R.: Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, Princeton (1994)

    Google Scholar 

  23. Mosterman, P.J.: An Overview of Hybrid Simulation Phenomena and their Support by Simulation Packages. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 165–177. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  24. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)

    Google Scholar 

  25. Maler, O., Pnueli, A.: On Recognizable Timed Languages. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 348–362. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  26. Pnueli, A.: Verification of Reactive Systems. Lecture Notes, NYU (2003), http://cs.nyu.edu/courses/fall03/G22.3033-007/lecture4.pdf

  27. Sokolsky, O., Viswanathan, M. (eds.): Runtime Verification RV 2003. ENTCS, vol. 89(2) (2003)

    Google Scholar 

  28. Thati, P., Rosu, G.: Monitoring Algorithms for Metric Temporal Logic Specifications. In: Proc. of RV 2004 (2004)

    Google Scholar 

  29. Tripakis, S.: Fault Diagnosis for Timed Automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 205–224. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  30. Vardi, M.Y., Wolper, P.: An Automata-theoretic Approach to Automatic Program Verification. In: Proc. LICS 1986, pp. 322–331. IEEE, Los Alamitos (1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. VERIMAG, 2 Av. de Vignate, 38610, Gières, France

    Oded Maler & Dejan Nickovic

Authors
  1. Oded Maler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dejan Nickovic
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. VERIMAG - University Joseph Fourier - CNRS - INPG, 2, av. de Vignates, 38610, Gières, France

    Yassine Lakhnech

  2. VERIMAG, Centre Equation, 2 av. de Vignate, 38610, Gieres, France

    Sergio Yovine

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Maler, O., Nickovic, D. (2004). Monitoring Temporal Properties of Continuous Signals. In: Lakhnech, Y., Yovine, S. (eds) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. FTRTFT FORMATS 2004 2004. Lecture Notes in Computer Science, vol 3253. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30206-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30206-3_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23167-7

  • Online ISBN: 978-3-540-30206-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation