Advertisement

A Service-Oriented Approach for Decomposing and Verifying Hybrid System Models

  • Timm LiebrenzEmail author
  • Paula Herber
  • Sabine Glesner
Conference paper
  • 23 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12018)

Abstract

The design of fault free hybrid control systems, which combine discrete and continuous behavior, is a challenging task. Their hybrid behavior and further factors make their design and verification challenging: These systems can consist of multiple interacting components, and commonly used design languages, like MATLAB Simulink do not directly allow for the verification of hybrid behavior. By providing hybrid contracts, which formally define the interface behavior of hybrid system components in differential dynamic logic ( Open image in new window ), and providing a decomposition technique, we enable compositional verification of Simulink models with interacting components. This enables us to use the interactive theorem prover KeYmaera X to prove the correctness of hybrid control systems modeled in Simulink, which we demonstrate with an automotive industrial case study.

Keywords

Hybrid systems Compositional verification Theorem proving Model-driven development 

References

  1. 1.
    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_30CrossRefGoogle Scholar
  2. 2.
    Araiza-Illan, D., Eder, K., Richards, A.: Formal verification of control systems’ properties with theorem proving. In: 2014 UKACC International Conference on Control (CONTROL), pp. 244–249. IEEE (2014)Google Scholar
  3. 3.
    Aştefănoaei, L., Bensalem, S., Bozga, M.: A compositional approach to the verification of hybrid systems. In: Ábrahám, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 88–103. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-30734-3_8CrossRefGoogle Scholar
  4. 4.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006).  https://doi.org/10.1007/11804192_17CrossRefGoogle Scholar
  5. 5.
    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)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Boström, P.: Contract-based verification of Simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 291–306. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-24559-6_21CrossRefGoogle Scholar
  7. 7.
    Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verification. In: IEEE Transactions on Automatic Control, vol. 48, pp. 64–75. IEEE (2003)Google Scholar
  8. 8.
    Cubuktepe, M., Ahmadi, M., Topcu, U., Hencey, B.: Compositional analysis of hybrid systems defined over finite alphabets. IFAC-PapersOnLine 51(16), 115–120 (2018)CrossRefGoogle Scholar
  9. 9.
    De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  10. 10.
    Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_8CrossRefGoogle Scholar
  11. 11.
    Frehse, G.: PHAVer: algorithmic verification of hybrid systems past hytech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31954-2_17CrossRefzbMATHGoogle Scholar
  12. 12.
    Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21401-6_36CrossRefGoogle Scholar
  13. 13.
    Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1, 110–122 (1997)CrossRefGoogle Scholar
  14. 14.
    Herber, P., Reicherdt, R., Bittner, P.: Bit-precise formal verification of discrete-time MATLAB/Simulink models using SMT solving. In: 2013 Proceedings of the International Conference on Embedded Software (EMSOFT), pp. 1–10. IEEE (2013)Google Scholar
  15. 15.
    Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 475–478. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27813-9_40CrossRefGoogle Scholar
  16. 16.
    Liebrenz, T., Herber, P., Glesner, S.: Deductive verification of hybrid control systems modeled in Simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 89–105. Springer, Cham (2018).  https://doi.org/10.1007/978-3-030-02450-5_6CrossRefGoogle Scholar
  17. 17.
    Liebrenz, T., Herber, P., Göthel, T., Glesner, S.: Towards service-oriented design of hybrid systems modeled in Simulink. In: 2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC), vol. 2, pp. 469–474. IEEE (2017)Google Scholar
  18. 18.
    MathWorks: MATLAB Simulink. www.mathworks.com/products/simulink.html
  19. 19.
    MathWorks: White Paper: Code Verification and Run-Time Error Detection Through Abstract Interpretation. Technical report (2008)Google Scholar
  20. 20.
    Minopoli, S., Frehse, G.: SL2SX translator: from Simulink to SpaceEx models. In: 19th International Conference on Hybrid Systems: Computation and Control, pp. 93–98. ACM (2016)Google Scholar
  21. 21.
    Mitsch, S., Platzer, A.: The KeYmaera X proof IDE: concepts on usability in hybrid systems theorem proving. In: 3rd Workshop on Formal Integrated Development Environment. Electronic Proceedings in Theoretical Computer Science, vol. 240, pp. 67–81. Open Publishing Association (2017)Google Scholar
  22. 22.
    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.) FASE 2017. LNCS, vol. 10202, pp. 134–151. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54494-5_8CrossRefGoogle Scholar
  23. 23.
    O’Halloran, C.: Automated verification of code automatically generated from Simulink®. Autom. Softw. Eng. 20(2), 237–264 (2013)CrossRefGoogle Scholar
  24. 24.
    Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219–265 (2017)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Reicherdt, R., Glesner, S.: Formal verification of discrete-time MATLAB/Simulink models using boogie. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 190–204. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10431-7_14CrossRefGoogle Scholar
  27. 27.
    Sanfelice, R., Copp, D., Nanez, P.: A toolbox for simulation of hybrid systems in Matlab/Simulink: Hybrid Equations (HyEQ) toolbox. In: 16th International Conference on Hybrid Systems: Computation and Control, pp. 101–106. ACM (2013)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Software and Embedded Systems Engineering GroupTU BerlinBerlinGermany
  2. 2.Embedded Systems GroupUniversity of MünsterMünsterGermany

Personalised recommendations