Document Open Access Logo

A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors Eduard Kamburjan , Stefan Mitsch , Reiner Hähnle

PDF
Thumbnail PDF

File

LITES.8.2.4.pdf
  • Filesize: 1.36 MB
  • 34 pages

Document Identifiers

Author Details

Eduard Kamburjan
  • Department of Informatics, University of Oslo, Norway
  • Department of Computer Science, Technische Universität Darmstadt, Germany
Stefan Mitsch
  • Computer Science Department, Carnegie Mellon University, USA
Reiner Hähnle
  • Department of Computer Science, Technische Universität Darmstadt, Germany

Cite As Get BibTex

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LITES.8.2.4

Abstract

Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Distributed programming languages
  • Computing methodologies → Model verification and validation
  • Theory of computation → Logic and verification
  • Theory of computation → Timed and hybrid models
Keywords
  • Active Objects
  • Differential Dynamic Logic
  • Hybrid Systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Ehsan Ahmad, Yunwei Dong, Shuling Wang, Naijun Zhan, and Liang Zou. Adding formal meanings to AADL with hybrid annex. In Ivan Lanese and Eric Madelaine, editors, Formal Aspects of Component Software - 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers, volume 8997 of Lecture Notes in Computer Science, pages 228-247. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-15317-9_15.
  2. Ehsan Ahmad, Brian R. Larson, Stephen C. Barrett, Naijun Zhan, and Yunwei Dong. Hybrid annex: an AADL extension for continuous behavior and cyber-physical interaction modeling. In Michael Feldman and S. Tucker Taft, editors, Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014, pages 29-38. ACM, 2014. URL: https://doi.org/10.1145/2663171.2663178.
  3. Elvira Albert, Frank S. de Boer, Reiner Hähnle, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Peter Y. H. Wong. Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS. Service Oriented Computing and Applications, 8(4):323-339, 2014. Google Scholar
  4. M. Althoff. An introduction to CORA 2015. In Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems, 2015. Google Scholar
  5. Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, volume 736 of LNCS, pages 209-229, Berlin, Heidelberg, 1993. Springer. Google Scholar
  6. Rajeev Alur, Thao Dang, Joel M. Esposito, Rafael B. Fierro, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George J. Pappas, and Oleg Sokolsky. Hierarchical hybrid modeling of embedded systems. In Thomas A. Henzinger and Christoph M. Kirsch, editors, Embedded Software, First International Workshop, EMSOFT 2001, Tahoe City, CA, USA, October, 8-10, 2001, Proceedings, volume 2211 of Lecture Notes in Computer Science, pages 14-31. Springer, 2001. URL: https://doi.org/10.1007/3-540-45449-7_2.
  7. Rajeev Alur, Radu Grosu, Yerang Hur, Vijay Kumar, and Insup Lee. Modular specification of hybrid systems in CHARON. In Nancy A. Lynch and Bruce H. Krogh, editors, Hybrid Systems: Computation and Control, Third International Workshop, HSCC 2000, Pittsburgh, PA, USA, March 23-25, 2000, Proceedings, volume 1790 of Lecture Notes in Computer Science, pages 6-19. Springer, 2000. URL: https://doi.org/10.1007/3-540-46430-1_5.
  8. Sven Apel, Don S. Batory, Christian Kästner, and Gunter Saake. Feature-Oriented Software Product Lines - Concepts and Implementation. Springer, 2013. Google Scholar
  9. Paul C. Attie and Nancy A. Lynch. Dynamic input/output automata: A formal and compositional model for dynamic systems. Inf. Comput., 249:28-75, 2016. URL: https://doi.org/10.1016/j.ic.2016.03.008.
  10. Stanley Bak, Omar Ali Beg, Sergiy Bogomolov, Taylor T. Johnson, Luan Viet Nguyen, and Christian Schilling. Hybrid automata: from verification to implementation. STTT, 21(1):87-104, 2019. Google Scholar
  11. Stanley Bak, Sergiy Bogomolov, and Taylor T. Johnson. HYST: a source transformation and translation tool for hybrid automaton models. In Antoine Girard and Sriram Sankaranarayanan, editors, HSCC'15, pages 128-133. ACM, 2015. Google Scholar
  12. Richard Banach, Michael J. Butler, Shengchao Qin, Nitika Verma, and Huibiao Zhu. Core hybrid Event-B I: single hybrid Event-B machines. Sci. Comput. Program., 105:92-123, 2015. URL: https://doi.org/10.1016/j.scico.2015.02.003.
  13. Richard Banach, Michael J. Butler, Shengchao Qin, and Huibiao Zhu. Core hybrid Event-B II: multiple cooperating hybrid Event-B machines. Sci. Comput. Program., 139:1-35, 2017. URL: https://doi.org/10.1016/j.scico.2016.12.003.
  14. Don S. Batory, Jacob Neal Sarvela, and Axel Rauschmayer. Scaling step-wise refinement. IEEE Trans. Software Eng., 30(6):355-371, 2004. Google Scholar
  15. Luca Benvenuti, Davide Bresolin, Pieter Collins, Alberto Ferrari, Luca Geretti, and Tiziano Villa. Assume–guarantee verification of nonlinear hybrid systems with Ariadne. International Journal of Robust and Nonlinear Control, 24(4):699-724, 2014. URL: https://doi.org/10.1002/rnc.2914.
  16. Joakim Bjørk, Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, and Silvia Lizeth Tapia Tarifa. User-defined schedulers for real-time concurrent objects. Innovations in Systems and Software Engineering, 9(1):29-43, 2013. Google Scholar
  17. Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina S. Pasareanu, Andreas Podelski, and Thomas Strump. Assume-guarantee abstraction refinement meets hybrid systems. In Eran Yahav, editor, Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings, volume 8855 of Lecture Notes in Computer Science, pages 116-131. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-13338-6_10.
  18. Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer. VeriPhy: Verified controller executables from verified cyber-physical system models. In Dan Grossman, editor, PLDI, pages 617-630. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192406.
  19. Christopher X. Brooks, Edward A. Lee, David Lorenzetti, Thierry S. Nouidui, and Michael Wetter. CyPhySim: a cyber-physical systems simulator. In Antoine Girard and Sriram Sankaranarayanan, editors, HSCC'15, pages 301-302. ACM, 2015. URL: https://doi.org/10.1145/2728606.2728641.
  20. Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3):212-232, 2005. Google Scholar
  21. Michael J. Butler, Jean-Raymond Abrial, and Richard Banach. Modelling and refining hybrid systems in Event-B and Rodin. In Luigia Petre and Emil Sekerinski, editors, From Action Systems to Distributed Systems - The Refinement Approach, pages 29-42. Chapman and Hall/CRC, 2016. URL: https://doi.org/10.1201/b20053-5.
  22. Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei Yang, Naijun Zhan, Hengjun Zhao, and Liang Zou. MARS: A toolchain for modelling, analysis and verification of hybrid systems. In Michael G. Hinchey, Jonathan P. Bowen, and Ernst-Rüdiger Olderog, editors, Provably Correct Systems, NASA Monographs in Systems and Software Engineering, pages 39-58. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-48628-4_3.
  23. Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. Flow*: An analyzer for non-linear hybrid systems. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 258-263. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_18.
  24. Xin Chen and Sriram Sankaranarayanan. Decomposed reachability analysis for nonlinear systems. In 2016 IEEE Real-Time Systems Symposium, RTSS 2016, Porto, Portugal, November 29 - December 2, 2016, pages 13-24. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/RTSS.2016.011.
  25. Dave Clarke, Radu Muschevici, José Proença, Ina Schaefer, and Rudolf Schlatte. Variability modelling in the ABS language. In FMCO, volume 6957 of Lecture Notes in Computer Science, pages 204-224. Springer, 2010. Google Scholar
  26. Fabio Cremona, Marten Lohstroh, David Broman, Edward A. Lee, Michael Masin, and Stavros Tripakis. Hybrid co-simulation: it’s about time. Software and Systems Modeling, 18(3):1655-1679, 2019. URL: https://doi.org/10.1007/s10270-017-0633-6.
  27. P.J.L. Cuijpers and M.A. Reniers. Hybrid process algebra. J. of Logic and Algebraic Programming, 62(2):191-245, 2005. Google Scholar
  28. Frank S. de Boer, Dave Clarke, and Einar Broch Johnsen. A complete guide to the future. In ESOP, volume 4421 of Lecture Notes in Computer Science, pages 316-330. Springer, 2007. Google Scholar
  29. Frank S. de Boer, Vlad Serbanescu, Reiner Hähnle, Ludovic Henrio, Justine Rochas, Crystal Chang Din, Einar Broch Johnsen, Marjan Sirjani, Ehsan Khamespanah, Kiko Fernandez-Reyes, and Albert Mingkun Yang. A survey of active object languages. ACM Computíng Surveys, 50(5):1-39, 2017. Google Scholar
  30. Ankush Desai, Amar Phanishayee, Shaz Qadeer, and Sanjit A. Seshia. Compositional programming and testing of dynamic distributed systems. Proc. ACM Program. Lang., 2(OOPSLA):159:1-159:30, 2018. URL: https://doi.org/10.1145/3276529.
  31. Crystal Chang Din, Reiner Hähnle, Einar Broch Johnsen, Ka I Pun, and Silvia Lizeth Tapia Tarifa. Locally abstract, globally concrete semantics of concurrent programming languages. In Renate A. Schmidt and Cláudia Nalon, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings, volume 10501 of Lecture Notes in Computer Science, pages 22-43. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66902-1_2.
  32. Crystal Chang Din and Olaf Owe. Compositional reasoning about active objects with shared futures. Formal Asp. Comput., 27(3):551-572, 2015. URL: https://doi.org/10.1007/s00165-014-0322-y.
  33. Alexandre Donzé and Goran Frehse. Modular, hierarchical models of control systems in SpaceEx. In European Control Conference, ECC 2013, Zurich, Switzerland, July 17-19, 2013, pages 4244-4251. IEEE, 2013. URL: http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=6669815, URL: https://doi.org/10.23919/ECC.2013.6669815.
  34. Guillaume Dupont, Yamine Aït Ameur, Neeraj Kumar Singh, and Marc Pantel. Event-B hybridation: A proof and refinement-based framework for modelling hybrid systems. ACM Trans. Embed. Comput. Syst., 20(4):35:1-35:37, 2021. URL: https://doi.org/10.1145/3448270.
  35. Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. SpaceEx: Scalable verification of hybrid systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 379-395. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_30.
  36. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, CADE'25, volume 9195 of LNCS, pages 527-538. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_36.
  37. Sicun Gao, Soonho Kong, and Edmund M. Clarke. dReal: An SMT solver for nonlinear theories over the reals. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 208-214. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_14.
  38. Luis Garcia, Stefan Mitsch, and André Platzer. HyPLC: hybrid programmable logic controller program translation for verification. In ICCPS'19, pages 47-56, 2019. Google Scholar
  39. Sergey Goncharov and Renato Neves. An adequate while-language for hybrid computation. CoRR, abs/1902.07684, 2019. Google Scholar
  40. Sergey Goncharov, Renato Neves, and José Proença. Implementing hybrid semantics: From functional to imperative. In Violet Ka I Pun, Volker Stolz, and Adenilso Simão, editors, Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings, volume 12545 of Lecture Notes in Computer Science, pages 262-282. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64276-1_14.
  41. Daniel Grahl, Richard Bubel, Wojciech Mostowski, Peter H. Schmitt, Mattias Ulbrich, and Benjamin Weiß. Modular specification and verification. In Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors, Deductive Software Verification - The KeY Book - From Theory to Practice, volume 10001 of Lecture Notes in Computer Science, pages 289-351. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-49812-6_9.
  42. Ichiro Hasuo and Kohei Suenaga. Exercises in nonstandard static analysis of hybrid systems. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 462-478. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_34.
  43. Thomas A. Henzinger, Marius Minea, and Vinayak S. Prabhu. Assume-guarantee reasoning for hierarchical hybrid systems. In Maria Domenica Di Benedetto and Alberto L. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings, volume 2034 of Lecture Notes in Computer Science, pages 275-290. Springer, 2001. URL: https://doi.org/10.1007/3-540-45351-2_24.
  44. Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular ACTOR formalism for artificial intelligence. In IJCAI'73, pages 235-245, 1973. Google Scholar
  45. Jochen Hoenicke and Ernst-Rüdiger Olderog. Combining specification techniques for processes, data and time. In Michael Butler, Luigia Petre, and Kaisa Sere, editors, Integrated Formal Methods, pages 245-266, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. Google Scholar
  46. Iman Jahandideh, Fatemeh Ghassemi, and Marjan Sirjani. Hybrid Rebeca: modeling and analyzing of cyber-physical systems. CoRR, abs/1901.02597, 2019. URL: http://arxiv.org/abs/1901.02597.
  47. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer. A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. STTT, 19(6):717-741, 2017. URL: https://doi.org/10.1007/s10009-016-0434-1.
  48. Einar Broch Johnsen, Reiner Hähnle, Jan Schäfer, Rudolf Schlatte, and Martin Steffen. ABS: A core language for abstract behavioral specification. In Bernhard K. Aichernig, Frank S. de Boer, and Marcello M. Bonsangue, editors, FMCO'10, volume 6957 of LNCS, pages 142-164. Springer, 2010. Google Scholar
  49. Einar Broch Johnsen, Ka I Pun, and Silvia Lizeth Tapia Tarifa. A formal model of cloud-deployed software and its application to workflow processing. In Dinko Begusic, Nikola Rozic, Josko Radic, and Matko Saric, editors, SoftCOM'17, pages 1-6. IEEE, 2017. Google Scholar
  50. Eduard Kamburjan. Detecting deadlocks in formal system models with condition synchronization. ECEASST, 76, 2018. URL: https://doi.org/10.14279/tuj.eceasst.76.1070.
  51. Eduard Kamburjan. From post-conditions to post-region invariants: Deductive verification of hybrid objects. In HSCC. ACM, 2021. Google Scholar
  52. Eduard Kamburjan, Crystal Chang Din, Reiner Hähnle, and Einar Broch Johnsen. Behavioral contracts for cooperative scheduling. In 20 Years of KeY, volume 12345 of Lecture Notes in Computer Science, pages 85-121. Springer, 2020. Google Scholar
  53. Eduard Kamburjan, Reiner Hähnle, and Sebastian Schön. Formal modeling and analysis of railway operations with Active Objects. Science of Computer Programming, 166:167-193, November 2018. Google Scholar
  54. Eduard Kamburjan, Rudolf Schlatte, Einar Broch Johnsen, and S. Lizeth Tapia Tarifa. Designing distributed control with hybrid active objects. In ISoLA, volume 12479 of LNCS. Springer, 2020. Google Scholar
  55. Soonho Kong, Sicun Gao, Wei Chen, and Edmund M. Clarke. dReach: δ-reachability analysis for hybrid systems. In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science, pages 200-205. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46681-0_15.
  56. Jia-Chun Lin, Ingrid Chieh Yu, Einar Broch Johnsen, and Ming-Chang Lee. ABS-YARN: A formal framework for modeling hadoop YARN clusters. In Perdita Stevens and Andrzej Wasowski, editors, FASE'16, volume 9633 of LNCS, pages 49-65. Springer, 2016. Google Scholar
  57. Jiang Liu, Jidong Lv, Zhao Quan, Naijun Zhan, Hengjun Zhao, Chaochen Zhou, and Liang Zou. A calculus for hybrid CSP. In Kazunori Ueda, editor, Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Shanghai, China, November 28 - December 1, 2010. Proceedings, volume 6461 of Lecture Notes in Computer Science, pages 1-15. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17164-2_1.
  58. Simon Lunel, Stefan Mitsch, Benoît Boyer, and Jean-Pierre Talpin. Parallel composition and modular verification of computer controlled systems in differential dynamic logic. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods, The Next 30 Years, Third World Congress, FM, Porto, Portugal, volume 11800 of LNCS, pages 354-370. Springer, 2019. Google Scholar
  59. Nancy A. Lynch, Roberto Segala, and Frits W. Vaandrager. Hybrid I/O automata. Inf. Comput., 185(1):105-157, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00067-1.
  60. Brendan P. Mahony and Jin Song Dong. Deep semantic links of TCSP and Object-Z: TCOZ approach. Formal Aspects Comput., 13(2):142-160, 2002. URL: https://doi.org/10.1007/s001650200004.
  61. Maxima Manual, 5.43.0 edition, 2019. URL: maxima.sourceforge.net. Google Scholar
  62. Stefan Mitsch, Grant Olney Passmore, and André Platzer. Collaborative verification-driven engineering of hybrid systems. Math. Comput. Sci., 8(1):71-97, 2014. URL: https://doi.org/10.1007/s11786-014-0176-y.
  63. Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyber-physical system models. Form. Methods Syst. Des., 49(1):33-74, 2016. Google Scholar
  64. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, and André Platzer. Tactical contract composition for hybrid system component verification. STTT, 20(6):615-643, 2018. Special issue for selected papers from FASE'17. Google Scholar
  65. André Platzer. Differential-algebraic dynamic logic for differential-algebraic programs. J. of Logic and Computation, 20(1):309-352, 2010. Google Scholar
  66. André Platzer. The complete proof theory of hybrid systems. In LICS, pages 541-550. IEEE, 2012. Google Scholar
  67. André Platzer. The structure of differential invariants and differential cut elimination. Logical Methods in Computer Science, 8(4):1-38, 2012. URL: https://doi.org/10.2168/LMCS-8(4:16)2012.
  68. André Platzer. A complete uniform substitution calculus for differential dynamic logic. J. Automated Reasoning, 59(2):219-265, 2017. Google Scholar
  69. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Google Scholar
  70. André Platzer and Yong Kiam Tan. Differential equation invariance axiomatization. J. ACM, 67(1):6:1-6:66, 2020. URL: https://doi.org/10.1145/3380825.
  71. Claudius Ptolemaeus, editor. System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org, 2014. Google Scholar
  72. Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer. How to model and prove hybrid systems with KeYmaera: A tutorial on safety. STTT, 18(1):67-91, 2016. URL: https://doi.org/10.1007/s10009-015-0367-0.
  73. Ina Schaefer, Lorenzo Bettini, Viviana Bono, Ferruccio Damiani, and Nico Tanzarella. Delta-oriented programming of software product lines. In SPLC, volume 6287 of Lecture Notes in Computer Science, pages 77-91. Springer, 2010. Google Scholar
  74. Ina Schaefer, Rick Rabiser, Dave Clarke, Lorenzo Bettini, David Benavides, Goetz Botterweck, Animesh Pathak, Salvador Trujillo, and Karina Villela. Software diversity: state of the art and perspectives. STTT, 14(5):477-495, 2012. Google Scholar
  75. Rudolf Schlatte, Einar Broch Johnsen, Jacopo Mauro, Silvia Lizeth Tapia Tarifa, and Ingrid Chieh Yu. Release the beasts: When formal methods meet real world data. In It’s All About Coordination, volume 10865 of Lecture Notes in Computer Science, pages 107-121. Springer, 2018. Google Scholar
  76. Wen Su, Jean-Raymond Abrial, and Huibiao Zhu. Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program., 94:164-202, 2014. URL: https://doi.org/10.1016/j.scico.2014.04.015.
  77. Kohei Suenaga and Ichiro Hasuo. Programming with infinitesimals: A while-language for hybrid system modeling. In ICALP (2), volume 6756 of Lecture Notes in Computer Science, pages 392-403. Springer, 2011. Google Scholar
  78. Casper Thule, Kenneth Lausdahl, Cláudio Gomes, Gerd Meisl, and Peter Gorm Larsen. Maestro: The INTO-CPS co-simulation framework. Simulation Modelling Practice and Theory, 92:45-61, 2019. URL: https://doi.org/10.1016/j.simpat.2018.12.005.
  79. D. A. van Beek, Michel A. Reniers, Ramon R. H. Schiffelers, and J. E. Rooda. Foundations of a compositional interchange format for hybrid systems. In Alberto Bemporad, Antonio Bicchi, and Giorgio C. Buttazzo, editors, HSCC'07, volume 4416 of LNCS, pages 587-600. Springer, 2007. Google Scholar
  80. Shuling Wang, Naijun Zhan, and Liang Zou. An improved HHL prover: An interactive theorem prover for hybrid systems. In Michael Butler, Sylvain Conchon, and Fatiha Zaïdi, editors, Formal Methods and Software Engineering, pages 382-399, Cham, 2015. Springer International Publishing. Google Scholar
  81. Peter Y. H. Wong, Elvira Albert, Radu Muschevici, José Proença, Jan Schäfer, and Rudolf Schlatte. The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. STTT, 14(5):567-588, 2012. Google Scholar
  82. Zhenkai Zhang, Emeka Eyisi, Xenofon D. Koutsoukos, Joseph Porter, Gabor Karsai, and Janos Sztipanovits. A co-simulation framework for design of time-triggered automotive cyber physical systems. Simulation Modelling Practice and Theory, 43:16-33, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact