Skip to main content
SpringerLink
Log in

A Semantic Account of Rigorous Simulation

  • Chapter
  • First Online:
Principles of Modeling

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

  • 1720 Accesses

Abstract

Hybrid systems are a powerful formalism for modeling cyber-physical systems. Reachability analysis is a general method for checking safety properties, especially in the presence of uncertainty and non-determinism. Rigorous simulation is a convenient tool for reachability analysis of hybrid systems. However, to serve as proof tool, a rigorous simulator must be correct w.r.t. a clearly defined notion of reachability, which captures what is intuitively reachable in finite time.

As a step towards addressing this challenge, this paper presents a rigorous simulator in the form of an operational semantics and a specification in the form of a denotational semantics. We show that, under certain conditions about the representation of enclosures, the rigorous simulator is correct. We also show that finding a representation satisfying these assumptions is non-trivial.

Funded by USA National Science Foundation and Swedish Knowledge Foundation. Most of the work on this paper was done when the authors were at Halmstad Univ.

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.

    Edward A. Lee, First Halmstad Colloquium, Halmstad Univ., February 10th, 2012. Minutes 1:17-1:20 in video http://bit.ly/HC-EAL, paraphrased slightly for clarity.

References

  1. Acumen (2016). http://acumen-language.org

  2. Aljarbouh, A., Caillaud, B.: On the regularization of chattering executions in real time simulation of hybrid systems. In: Baltic Young Scientists Conference, p. 49 (2015)

    Google Scholar 

  3. Aljarbouh, A., Zeng, Y., Duracz, A., Caillaud, B., Taha, W.: Chattering-free simulation for hybrid dynamical systems. In: 2016 IEEE International Conference on Computational Science and Engineering, IEEE International Conference on Embedded and Ubiquitous Computing, and International Symposium on Distributed Computing and Applications to Business, Engineering and Science. IEEE Computer Society (2016)

    Google Scholar 

  4. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138, 3–34 (1995)

    Article  MathSciNet  Google Scholar 

  5. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57318-6_30

    Chapter  Google Scholar 

  6. Chabert, G., Jaulin, L.: Contractor programming. Artif. Intell. 173(11), 1079–1100 (2009)

    Article  MathSciNet  Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511–547 (1992)

    Article  MathSciNet  Google Scholar 

  8. Duracz, A.: Rigorous simulation: its theory and applications. Ph.D. thesis. Halmstad University Press (2016)

    Google Scholar 

  9. Duracz, A., Bartha, F.A., Taha, W.: Accurate rigorous simulation should be possible for good designs. In: 2016 International Workshop on Symbolic and Numerical Methods for Reachability Analysis, SNR, pp. 1–10. IEEE (2016)

    Google Scholar 

  10. Duracz, A., Eriksson, H., Bartha, F.A., Zeng, Y., Xu, F., Taha, W.: Using rigorous simulation to support ISO 26262 hazard analysis and risk assessment. In: 12th International Conference on Embedded Software and Systems, ICESS, pp. 1093–1096. IEEE (2015)

    Google Scholar 

  11. Goebel, R., Sanfelice, R.G., Teel, A.: Hybrid dynamical systems. IEEE Control Syst. 29(2), 28–93 (2009)

    Article  MathSciNet  Google Scholar 

  12. Henzinger, T.A.: The theory of hybrid automata. In: Logic in Computer Science, pp. 278–292. IEEE Computer Society, New Brunswick (1996)

    Google Scholar 

  13. Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Applied Interval Analysis: With Examples in Parameter and State Estimation, Robust Control and Robotics. Springer, London (2001). https://doi.org/10.1007/978-1-4471-0249-6

    Book  MATH  Google Scholar 

  14. Johansson, K.H., Egerstedt, M., Lygeros, J., Sastry, S.: On the regularization of Zeno hybrid automata. Syst. Control Lett. 38(3), 141–150 (1999)

    Article  MathSciNet  Google Scholar 

  15. Konečnỳ, M., Taha, W., Bartha, F.A., Duracz, J., Duracz, A., Ames, A.D.: Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point. Nonlinear Anal.: Hybrid Syst. 20, 1–20 (2016)

    MathSciNet  MATH  Google Scholar 

  16. Konečný, M., Taha, W., Duracz, J., Duracz, A., Ames, A.: Enclosing the behavior of a hybrid system up to and beyond a Zeno point. In: 1st IEEE International Conference on Cyber-Physical Systems, Networks, and Applications, CPSNA, pp. 120–125 (2013)

    Google Scholar 

  17. Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems: A Cyber-Physical Systems Approach. MIT Press, Cambridge (2016)

    MATH  Google Scholar 

  18. Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 25–53. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31954-2_2

    Chapter  Google Scholar 

  19. Lygeros, J.: Lecture notes on hybrid systems. In: Notes for an ENSIETA Workshop (2004). Sect. 4.2

    Google Scholar 

  20. Moggi, E., Farjudian, A., Duracz, A., Taha, W.: Safe & robust reachability analysis of hybrid systems. Theor. Comput. Sci. (2018). https://doi.org/10.1016/j.tcs.2018.06.020

  21. Moore, R.E.: Interval Analysis, vol. 4. Prentice-Hall, Upper Saddle River (1966)

    Google Scholar 

  22. Taha, W., Brauner, P., Zeng, Y., Cartwright, R., Gaspes, V., Ames, A., Chapoutot, A.: A core language for executable models of cyber-physical systems (preliminary report). In: 32nd International Conference on Distributed Computing Systems, pp. 303–308. IEEE (2012)

    Google Scholar 

  23. Tucker, W.: Validated Numerics: A Short Introduction to Rigorous Computations. Princeton University Press, Princeton (2011)

    MATH  Google Scholar 

  24. Zeng, Y., Bartha, F., Taha, W.: Compile-time extensions to hybrid ODEs. In: Ábrahám, E., Bogomolov, S. (eds.) Proceedings of 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, Uppsala, Sweden. Electronic Proceedings in Theoretical Computer Science, vol. 247, pp. 52–70. Open Publishing Association (2017)

    Article  Google Scholar 

  25. Zeng, Y., Chad, R., Taha, W., Duracz, A., Atkinson, K., Philippsen, R., Cartwright, R., O’Malley, M.: Modeling electromechanical aspects of cyber-physical systems. J. Softw. Eng. Robot. 7(1), 100–119 (2016)

    Google Scholar 

  26. Zhang, J., Johansson, K.H., Lygeros, J., Sastry, S.: Zeno hybrid systems. Int. J. Robust Nonlinear Control 11(5), 435–451 (2001)

    Article  MathSciNet  Google Scholar 

  27. Zheng, H., Lee, E.A., Ames, A.D.: Beyond Zeno: get on with It!. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 568–582. Springer, Heidelberg (2006). https://doi.org/10.1007/11730637_42

    Chapter  Google Scholar 

  28. Zhu, Y., Westbrook, E., Inoue, J., Chapoutot, A., Salama, C., Peralta, M., Martin, T., Taha, W., O’Malley, M., Cartwright, R., et al.: Mathematical equations as executable models of mechanical systems. In: Proceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems, pp. 1–11. ACM (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Rice University, Houston, TX, USA

    Adam Duracz

  2. DIBRIS, Genova University, Genova, Italy

    Eugenio Moggi

  3. Halmstad University, Halmstad, Sweden

    Walid Taha

  4. Zhejiang University, Hangzhou, China

    Zhenchao Lin

Authors
  1. Adam Duracz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eugenio Moggi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Walid Taha
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Zhenchao Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Walid Taha .

Editor information

Editors and Affiliations

  1. University of California, Berkeley, Berkeley, California, USA

    Marten Lohstroh

  2. National Instruments, Berkeley, California, USA

    Patricia Derler

  3. Mälardalen University, Västerås, Sweden, Reykjavík University, Reykjavik, Iceland

    Marjan Sirjani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Duracz, A., Moggi, E., Taha, W., Lin, Z. (2018). A Semantic Account of Rigorous Simulation. In: Lohstroh, M., Derler, P., Sirjani, M. (eds) Principles of Modeling. Lecture Notes in Computer Science(), vol 10760. Springer, Cham. https://doi.org/10.1007/978-3-319-95246-8_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95246-8_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95245-1

  • Online ISBN: 978-3-319-95246-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation