nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

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

verfasst von : Timm Liebrenz, Paula Herber, Sabine Glesner

Erschienen in: Formal Aspects of Component Software

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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 (

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-40914-2_7/MediaObjects/484177_1_En_7_Figa_HTML.gif

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

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Multilabeled Petri Nets

Nächstes Kapitel Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata

The

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-40914-2_7/MediaObjects/484177_1_En_7_Figap_HTML.gif

models and proofs of the temperature control system are available online: https://www.sese.tu-berlin.de/ServiceVerification/parameter/en/.

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_30CrossRef

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)

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_8CrossRef

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_17CrossRef

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

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_21CrossRef

Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verification. In: IEEE Transactions on Automatic Control, vol. 48, pp. 64–75. IEEE (2003)

Cubuktepe, M., Ahmadi, M., Topcu, U., Hencey, B.: Compositional analysis of hybrid systems defined over finite alphabets. IFAC-PapersOnLine 51(16), 115–120 (2018)CrossRef

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_24CrossRef

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_8CrossRef

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_17CrossRefMATH

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_36CrossRef

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

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)

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_40CrossRef

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_6CrossRef

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)

18.

MathWorks: MATLAB Simulink. www.mathworks.com/products/simulink.html

19.

MathWorks: White Paper: Code Verification and Run-Time Error Detection Through Abstract Interpretation. Technical report (2008)

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)

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)

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_8CrossRef

23.

O’Halloran, C.: Automated verification of code automatically generated from Simulink®. Autom. Softw. Eng. 20(2), 237–264 (2013)CrossRef

24.

Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008)MathSciNetCrossRef

25.

Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219–265 (2017)MathSciNetCrossRef

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_14CrossRef

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)

Titel: A Service-Oriented Approach for Decomposing and Verifying Hybrid System Models
verfasst von: Timm Liebrenz
Paula Herber
Sabine Glesner
Verlag: Springer International Publishing
Buch: Formal Aspects of Component Software
Print ISBN: 978-3-030-40913-5

Electronic ISBN: 978-3-030-40914-2

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-40914-2_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"