nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Combining Forces: How to Formally Verify Informally Defined Embedded Systems

verfasst von : Paula Herber, Timm Liebrenz, Julius Adelt

Erschienen in: Formal Methods

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

Embedded systems are ubiquitous in our daily lives, and they are often used in safety-critical applications, such as cars, airplanes, or medical systems. As a consequence, there is a high demand for formal methods to ensure their safety. Embedded systems are, however, concurrent, real-time dependent, and highly heterogeneous. Hardware and software are deeply intertwined, and the digital control parts interact with an analogous environment. Moreover, the semantics of industrially used embedded system design languages, such as MATLAB/Simulink or SystemC, is typically only informally defined. To formally capture informally defined embedded systems requires a deep understanding of the underlying models of computation. Furthermore, a single formalism and verification tool are typically not powerful enough to cope with the heterogeneity of embedded systems. In this paper, we summarize our work on automated transformations from informal system descriptions into existing formal verification tools. We present ideas to combine the strengths of various languages, formalisms, and verification backends, and discuss promising results, challenges and limitations.

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

Nächstes Kapitel Model Checking for Verification of Quantum Circuits

Several of our case studies and our Simulink2dL transformation are freely available at https://www.uni-muenster.de/EmbSys/research/Simulink2dL.

Adelt, J., Liebrenz, T., Herber, P.: Formal verification of intelligent hybrid systems that are modeled with Simulink and the reinforcement learning toolbox. In: Huisman, M., et al. (eds.) FM 2021, LNCS 13047, pp. 349–366. Springer, Heidelberg (2021)

Araiza-Illan, D., Eder, K., Richards, A.: Formal verification of control systems’ properties with theorem proving. In: UKACC International Conference on Control (CONTROL), pp. 244–249. IEEE (2014)

Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7CrossRef

Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16CrossRef

Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127–131. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_9CrossRef

Chen, M., et al.: MARS: a toolchain for modelling, analysis and verification of hybrid systems. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE, pp. 39–58. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-48628-4_3CrossRef

Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verification. IEEE Trans. Automa. Control. 48(1), 64–75 (2003). IEEEMathSciNetCrossRef

Cimatti, A., Micheli, A., Narasamdya, I., Roveri, M.: Verifying SystemC: a software model checking approach. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 51–59. IEEE (2010)

Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos – a software model checker for SystemC. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 310–316. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_24CrossRef

10.

Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking SystemC. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 32(5), 774–787 (2013)CrossRef

11.

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

12.

Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: toward safe control through proof and learning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)

13.

Garavel, H., Helmstetter, C., Ponsini, O., Serwe, W.: Verification of an industrial SystemC/TLM model using LOTOS and CADP. In: IEEE/ACM International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2009), pp. 46–55 (2009)

14.

Große, D., Kühne, U., Drechsler, R.: HW/SW co-verification of embedded systems using bounded model checking. In: Great Lakes Symposium on VLSI, pp. 43–48. ACM Press (2006)

15.

Große, D., Le, H.M., Drechsler, R.: Proving transaction and system-level properties of untimed SystemC TLM designs. In: MEMOCODE, pp. 113–122. IEEE (2010)

16.

Große, D., Le, H.M., Drechsler, R.: Formal verification of SystemC-based cyber components. In: Jeschke, S., Brecher, C., Song, H., Rawat, D.B. (eds.) Industrial Internet of Things. SSWT, pp. 137–167. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-42559-7_6CrossRef

17.

Habibi, A., Moinudeen, H., Tahar, S.: Generating finite state machines from SystemC. In: Design, Automation and Test in Europe, pp. 76–81. IEEE (2006)

18.

Habibi, A., Tahar, S.: An approach for the verification of SystemC designs using AsmL. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 69–83. Springer, Heidelberg (2005). https://doi.org/10.1007/11562948_8CrossRefMATH

19.

Herber, P.: The RESCUE approach - towards compositional hardware/software co-verification. In: International Conference on Embedded Software and Systems (ICESS 2014). pp. 721–724. IEEE (2014)

20.

Herber, P., Fellmuth, J., Glesner, S.: Model checking SystemC designs using timed automata. In: International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), pp. 131–136. ACM press (2008)

21.

Herber, P., Glesner, S.: A HW/SW co-verification framework for SystemC. ACM Trans. Embedd. Comput. Syst. (TECS) 12(1s), 1–23 (2013)CrossRef

22.

Herber, P., Hünnemeyer, B.: Formal verification of SystemC designs using the BLAST software model checker. In: ACESMB@ MoDELS, pp. 44–53 (2014)

23.

Herber, P., Liebrenz, T.: Dependence analysis and automated partitioning for scalable formal analysis of SystemC designs. In: 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), pp. 1–6. IEEE (2020)

24.

Herber, P., Pockrandt, M., Glesner, S.: STATE - a SystemC to timed automata transformation engine. In: ICESS. IEEE (2015)

25.

Herber, P., Reicherdt, R., Bittner, P.: Bit-precise formal verification of discrete-time MATLAB/Simulink models using SMT solving. In: International Conference on Embedded Software (EMSOFT), pp. 1–10. IEEE (2013)

26.

Herdt, V., Le, H.M., Grosse, D., Drechsler, R.: Verifying SystemC using intermediate verification language and stateful symbolic simulation. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 38(7), 1359–1372 (2018)CrossRef

27.

IEEE Standards Association: IEEE Std. 1666–2011, Open SystemC Language Reference Manual. IEEE Press (2011)

28.

Jaß, L., Herber, P.: Bit-precise formal verification for SystemC using satisfiability modulo theories solving. In: Götz, M., Schirner, G., Wehrmeister, M.A., Al Faruque, M.A., Rettberg, A. (eds.) IESS 2015. IAICT, vol. 523, pp. 51–63. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-90023-0_5CrossRef

29.

Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC designs using a Petri-Net based representation. In: Design, Automation and Test in Europe (DATE), pp. 1228–1233. IEEE Press (2006)

30.

Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects of Comput. 27(3), 573–609 (2015). https://doi.org/10.1007/s00165-014-0326-7MathSciNetCrossRef

31.

Kroening, D., Sharygina, N.: Formal verification of SystemC by automatic hardware/software partitioning. In: Proceedings of MEMOCODE 2005, pp. 101–110. IEEE (2005)

32.

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

33.

Le, H.M., Grosse, D., Herdt, V., Drechsler, R.: Verifying SystemC using an intermediate verification language and symbolic simulation. In: Design Automation Conference (DAC), 2013 50th ACM/EDAC/IEEE, pp. 1–6. IEEE (2013)

34.

Li, J., Sun, X., Xie, F., Song, X.: Component-based abstraction and refinement. In: Mei, H. (ed.) ICSR 2008. LNCS, vol. 5030, pp. 39–51. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68073-4_4CrossRef

35.

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

36.

Liebrenz, T., Herber, P., Glesner, S.: A service-oriented approach for decomposing and verifying hybrid system models. In: Arbab, F., Jongmans, S.-S. (eds.) FACS 2019. LNCS, vol. 12018, pp. 127–146. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-40914-2_7CrossRef

37.

Liebrenz, T., Herber, P., Glesner, S.: Towards automated service-oriented verification of embedded control software modeled in Simulink. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020, Part III. LNCS, vol. 12478, pp. 307–325. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-61467-6_20CrossRef

38.

Liebrenz, T., Herber, P., Glesner, S.: Service-oriented decomposition and verification of hybrid system models using feature models and contracts. Sci. Comput. Program. 211, 102694 (2021)CrossRef

39.

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)

40.

Liebrenz, T., Klös, V., Herber, P.: Automatic analysis and abstraction for model checking HW/SW co-designs modeled in SystemC. In: ACM SIGAda Annual Conference on High Integrity Language Technology (HILT 2016). ACM (2016)

41.

Man, K.L., Fedeli, A., Mercaldi, M., Boubekeur, M., Schellekens, M.: SC2SCFL: automated SystemC to \(SystemC^{\mathbb{FL}}\) translation. In: Vassiliadis, S., Bereković, M., Hämäläinen, T.D. (eds.) SAMOS 2007. LNCS, vol. 4599, pp. 34–45. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73625-7_6CrossRef

42.

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

43.

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

44.

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)

45.

Niemann, B., Haubelt, C., Oyanguren, M.U.: Formalizing TLM with communicating state machines. In: Huss, S.A. (ed.) Advances in Design and Specification Languages for Embedded Systems. Springer, Dordrecht (2007). https://doi.org/10.1007/978-1-4020-6149-3_14CrossRef

46.

Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143–189 (2008). https://doi.org/10.1007/s10817-008-9103-8MathSciNetCrossRefMATH

47.

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

48.

Ruf, J., Hoffmann, D.W., Gerlach, J., Kropf, T., Rosenstiel, W., Müller, W.: The simulation semantics of SystemC. In: Design, Automation and Test in Europe, pp. 64–70. IEEE Press (2001)

49.

Salem, A.: Formal semantics of synchronous SystemC. In: Design, Automation and Test in Europe (DATE). pp. 10376–10381. IEEE Computer Society (2003)

50.

Traulsen, C., Cornet, J., Moy, M., Maraninchi, F.: A SystemC/TLM semantics in Promela and its possible applications. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 204–222. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73370-6_14CrossRef

51.

Xie, F., Yang, G., Song, X.: Component-based hardware/software co-verification for building trustworthy embedded systems. J. Syst. Softw. 80(5), 643–654 (2007)CrossRef

52.

Yan, G., Jiao, L., Wang, S., Wang, L., Zhan, N.: Automatically generating SystemC code from HCSP formal models. ACM Trans. Softw. Eng. Methodol. (TOSEM) 29(1), 1–39 (2020)CrossRef

53.

Zhang, Y., Vedrine, F., Monsuez, B.: SystemC waiting-state automata. In: International Workshop on Verification and Evaluation of Computer and Communication Systems (2007)

54.

Zou, L., Zhan, N., Wang, S., Fränzle, M.: Formal verification of Simulink/Stateflow diagrams. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 464–481. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24953-7_33CrossRefMATH

Titel: Combining Forces: How to Formally Verify Informally Defined Embedded Systems
verfasst von: Paula Herber
Timm Liebrenz
Julius Adelt
Verlag: Springer International Publishing
Buch: Formal Methods
Print ISBN: 978-3-030-90869-0

Electronic ISBN: 978-3-030-90870-6

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-90870-6_1

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"

Premium Partner