Abstract
We present an approach for hybrid systems that combines the advantages of component-based modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Component-based modeling can be used to split large models into multiple component models with local responsibilities to reduce modeling complexity. Yet, this only helps the analysis if verification proceeds one component at a time. In order to benefit from the decomposition of a system into components for both modeling and verification purposes, we prove that the safety of compatible components implies safety of the composed system. We implement our composition theorem as a tactic in the KeYmaera X theorem prover, allowing automatic generation of a KeYmaera X proof for the composite system from proofs for the components without soundness-critical changes to KeYmaera X. Our approach supports component contracts (i.e., input assumptions and output guarantees for each component) that characterize the magnitude and rate of change of values exchanged between components. These contracts can take into account what has changed between two components in a given amount of time since the last exchange of information.
Article PDF
We’re sorry, something doesn't seem to be working properly.
Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.
Avoid common mistakes on your manuscript.
References
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.) Hybrid Systems, pp. 209–229. Lecture Notes in Computer Science, Springer, New York (1993)
Aştefanoaei, L., Bensalem, S., Bozga, M.: A compositional approach to the verification of hybrid systems. In: Ábrahám, E., Bonsangue, M., Johnsen, B.E. (eds.) Theory and Practice of Formal Methods, vol. 9660, pp. 88–103. Springer, New York (2016)
Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: Boer, F.S.d., Bonsangue, M.M., Graf, S., Roever, W.P.d. (eds.) Formal Methods for Components and Objects, 6th International Symposium, pp. 200–225. Lecture Notes in Computer Science, Springer, New York (2007)
Benvenuti, L., Bresolin, D., Collins, P., Ferrari, A., Geretti, L., Villa, T.: Assume-guarantee verification of nonlinear hybrid systems with Ariadne. Int. J. Robust Nonlinear Control 24(4), 699–724 (2014)
Bornot, S., Sifakis, J.: On the composition of hybrid systems. In: Henzinger, T.A., Sastry, S. (eds.) Hybrid Systems: Computation and Control, First International Workshop, Proceedings, pp. 49–63. Lecture Notes in Computer Science, Springer, New York (1998)
Cuijpers, P.J.L., Reniers, M.A.: Hybrid process algebra. J. Log. Algebr. Program. 62(2), 191–245 (2005)
Damm, W., Dierks, H., Oehlerking, J., Pnueli, A.: Towards component based design of hybrid systems: Safety and stability. In: Manna, Z., Peled, D.A. (eds.) Time for Verification, Essays in Memory of Amir Pnueli, vol. 6200, pp. 96–143. Lecture Notes in Computer Science, Springer, New York (2010)
Felty, A., Middeldorp, A. (eds.) International Conference on Automated Deduction, CADE’15, Berlin, Germany, Proceedings, vol. 9195. Lecture Notes in Computer Science, Springer, New York (2015)
Frehse, G., Zhi Han, Krogh, B.: Assume-guarantee reasoning for hybrid I/O-automata by over-approximation of continuous interaction. In: 43rd IEEE Conference on Decision and Control, CDC, vol. 1, pp. 479–484 (2004)
Fulton, N., Mitsch, S., Quesel, J.D., Völp, M., Platzer, A.: KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In: Felty and Middeldorp [8], pp. 527–538
Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)
Gößler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program. 55(1–3), 161–183 (2005)
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278–292. IEEE Computer Society (1996)
Henzinger, T.A., Minea, M., Prabhu, V.S.: Assume-guarantee reasoning for hierarchical hybrid systems. In: Benedetto, D., Domenica, M., Sangiovanni-Vincentelli, A.L. (eds.) Hybrid Systems: Computation and Control, 4th International Workshop, Proceedings, vol. 2034, pp. 275–290. Lecture Notes in Computer Science, Springer, New York (2001)
Loos, S.M., Platzer, A.: Differential refinement logic. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, Proceedings, pp. 505–514. ACM (2016)
Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) 17th International Symposium on Formal Methods, FM 2011, Proceedings, vol. 6664, pp. 42–56. Lecture Notes in Computer Science, Springer, New York (2011)
Lunel, S., Boyer, B., Talpin, J.P.: Compositional proofs in differential dynamic logic dL. In: 17th International Conference on Application of Concurrency to System Design, Proceedings, pp. 19–28. IEEE Computer Society (2017)
Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I/O automata. Inf. Comput. 185(1), 105–157 (2003)
Man, K.L., Reniers, M.A., Cuijpers, P.J.L.: Case studies in the hybrid process algebra Hypa. Int. J. Softw. Eng. Knowl. Eng. 15(2), 299–306 (2005)
Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. Int. J. Robot. Res. 36(12), 1312–1340 (2017)
Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Form. Methods Syst. Des. 49(1), 33–74 (2016). special issue of selected papers from RV’14
Moura, L.M.d., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, Proceedings, pp. 337–340. Lecture Notes in Computer Science, Springer, New York (2008)
Müller, A., Mitsch, S., Platzer, A.: Verified traffic networks: component-based verification of cyber-physical flow systems. In: 18th International Conference on Intelligent Transportation Systems, pp. 757–764 (2015)
Müller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: A component-based approach to hybrid systems safety verification. In: Abraham, E., Huisman, M. (eds.) Integrated Formal Methods—12th International Conference, IFM 2016, Proceedings, vol. 9681, pp. 441–456. Lecture Notes in Computer Science, Springer, New York (2016)
Müller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: A benchmark for component-based hybrid systems safety verification. In: Frehse, G., Althoff, M. (eds.) 4th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol. 48, pp. 65–74. EasyChair (2017)
Müller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: Change and delay contracts for hybrid system component verification. In: Huisman, M., Rubin, J. (eds.) Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings, vol. 10202, pp. 134–151. Lecture Notes in Computer Science, Springer, New York (2017)
Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Commun. ACM 15(12), 1053–1058 (1972)
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2), 143–189 (2008)
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)
Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. Log. Meth. Comput. Sci. 8(4), 1–44 (2012) (special issue for selected papers from CSL’10)
Platzer, A.: The complete proof theory of hybrid systems. In: Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, pp. 541–550. IEEE, Dubrovnik, 25–28 June 2012 (2012)
Platzer, A.: Logics of dynamical systems. In: Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, pp. 13–24. IEEE, Dubrovnik, 25–28 June 2012 (2012)
Platzer, A.: The structure of differential invariants and differential cut elimination. Log. Meth. Comput. Sci. 8(4), 1–38 (2012)
Platzer, A.: A uniform substitution calculus for differential dynamic logic. In: Felty and Middeldorp [8], pp. 467–481
Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas. 59(2), 219–265 (2017)
Platzer, A., Quesel, J.D.: European Train Control System: A case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Proceedings, vol. 5885, pp. 246–265. Lecture Notes in Computer Science, Springer, New York (2009)
Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: Dawar, A., Grädel, E. (eds.) Logic in Computer Science. ACM, New York (2018)
Ramon, R.H. Schiffelers, D.A., van Beek, Man, K.L., Reniers, M.A., Rooda, J.E.: Formal semantics of Hybrid Chi. In: Larsen, K.G., Niebert, P. (eds.) Formal Modeling and Analysis of Timed Systems: First International Workshop. pp. 151–165. Lecture Notes in Computer Science, Springer, New York (2003)
Rounds, W.C., Song, H.: The Phi-Calculus: A language for distributed control of reconfigurable embedded systems. In: Maler, O., Pnueli, A. (eds.) 6th International Workshop on Hybrid Systems: Computation and Control, pp. 435–449. Lecture Notes in Computer Science, Springer, New York (2003)
Ruchkin, I., Schmerl, B., Garlan, D.: Architectural abstractions for hybrid programs. In: Kruchten, P., Becker, S., Schneider, J. (eds.) Proceedings of the 18th International Symposium on Component-Based Software Engineering, pp. 65–74. CBSE’15, ACM (2015)
Schreiter, L., Bresolin, D., Capiluppi, M., Raczkowsky, J., Fiorini, P., Wörn, H.: Application of contract-based verification techniques for hybrid automata to surgical robotic systems. In: European Control Conference, ECC 2014, pp. 2310–2315. IEEE (2014)
Song, H., Compton, K.J., Rounds, W.C.: SPHIN: A model checker for reconfigurable hybrid systems based on SPIN. Electron. Notes Theor. Comput. Sci. 145, 167–183 (2006)
UML Revision Task Force: OMG unified modeling language specification, version 2.5: OMG document number: formal/15-03-01, http://www.omg.org/spec/UML/2.5/
Xinyu, C., Huiqun, Y., Xin, X.: Verification of Hybrid Chi model for cyber-physical systems using PHAVer. In: Barolli, L., You, I., Xhafa, F., Leu, F.Y., Chen, H.C. (eds.) Seventh International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing, pp. 122–128. IEEE Computer Society (2013)
Acknowledgments
Open access funding provided by JohannesKepler University Linz.
Author information
Authors and Affiliations
Corresponding authors
Additional information
This material is based on research sponsored by DARPA under agreement DARPA FA8750-12-2-0291, AFOSR FA9550-16-1-0288, and by the Austrian Science Fund (FWF) P28187-N31.
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Müller, A., Mitsch, S., Retschitzegger, W. et al. Tactical contract composition for hybrid system component verification. Int J Softw Tools Technol Transfer 20, 615–643 (2018). https://doi.org/10.1007/s10009-018-0502-9
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-018-0502-9