nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations

verfasst von : Viorel Preoteasa, Iulia Dragomir, Stavros Tripakis

Erschienen in: Verification, Model Checking, and Abstract Interpretation

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

Hierarchical block diagrams (HBDs) are at the heart of embedded system design tools, including Simulink. Numerous translations exist from HBDs into languages with formal semantics, amenable to formal verification. However, none of these translations has been proven correct, to our knowledge.

We present in this paper the first mechanically proven HBD translation algorithm. The algorithm translates HBDs into an algebra of terms with three basic composition operations (serial, parallel, and feedback). In order to capture various translation strategies resulting in different terms achieving different tradeoffs, the algorithm is nondeterministic. Despite this, we prove its semantic determinacy: for every input HBD, all possible terms that can be generated by the algorithm are semantically equivalent. We apply this result to show how three Simulink translation strategies introduced previously can be formalized as determinizations of the algorithm, and derive that these strategies yield semantically equivalent results (a question left open in previous work). All results are formalized and proved in the Isabelle theorem-prover and the code is publicly available.

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 Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics

Rahim, L.A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015)CrossRef

Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink/stateflow models to hybrid automata using graph transformations. Electron. Notes Theor. Comput. Sci. 109, 43–56 (2004)CrossRef

Amrani, M., et al.: Formal verification techniques for model transformations: a tridimensional classification. J. Object Technol. 14(3), 1:1–43 (2015)CrossRef

Auger, C.: Compilation certifiée de SCADE/LUSTRE. (Certified compilation of SCADE/LUSTRE). Ph.D. thesis, University of Paris-Sud, Orsay, France (2013). (in French)

Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998). https://doi.org/10.1007/978-1-4612-1674-2CrossRefMATH

Baez, J.C., Erbele, J.: Categories in control. CoRR, abs/1405.6881 (2015)

Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123–153 (2014)MathSciNetCrossRef

Berry, G.: The constructive semantics of pure Esterel (1999)

Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. SIGPLAN Not. 47(5), 129–138 (2012)

10.

Bourke, T., Brun, L., Dagand, P.É., Leroy, X., Pouzet, M., Rieg, L.: A formally verified compiler for lustre. SIGPLAN Not. 52(6), 586–601 (2017)CrossRef

11.

Calegari, D., Szasz, N.: Verification of model transformations. Electron. Notes Theor. Comput. Sci. 292, 5–25 (2013)CrossRef

12.

Chen, C., Dong, J.S., Sun, J.: A formal framework for modeling and validating Simulink diagrams. Form. Asp. Comput. 21(5), 451–483 (2009)CrossRef

13.

Courcelle, B.: A representation of graphs by algebraic expressions and its use for graph rewriting systems. In: Ehrig, H., Nagl, M., Rozenberg, G., Rosenfeld, A. (eds.) Graph Grammars 1986. LNCS, vol. 291, pp. 112–132. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-18771-5_49CrossRef

14.

Ştefănescu, G.: Network Algebra. Springer, London (2000). https://doi.org/10.1007/978-1-4471-0479-7CrossRefMATH

15.

Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)MathSciNetCrossRef

16.

Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional semantics and analysis of hierarchical block diagrams. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 38–56. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-32582-8_3CrossRef

17.

Dragomir, I., Preoteasa, V., Tripakis, S.: The refinement calculus of reactive systems toolset. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 201–208. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_12CrossRef

18.

Dragomir, I., Preoteasa, V., Tripakis, S.: The refinement calculus of reactive systems toolset - February 2018. Figshare. https://doi.org/10.6084/m9.figshare.5900911. Accessed Feb 2018

19.

Eclipse: ATL - a model transformation technology. http://www.eclipse.org/atl/

20.

Edwards, S., Lee, E.A.: The semantics and execution of a synchronous block-diagram language. Sci. Comput. Prog. 48, 21–42(22) (2003)MathSciNetCrossRef

21.

Ghica, D.R., Jung, A.: Categorical semantics of digital circuits. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, 3–6 October 2016, pp. 41–48. IEEE (2016)

22.

Ghica, D.R., Jung, A., Lopez, A.: Diagrammatic semantics for digital circuits. In: Goranko, V., Dam, M. (eds.) 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, LIPIcs, Stockholm, Sweden, vol. 82, pp. 24:1–24:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)

23.

Ghica, D.R., Lopez, A.: A structural and nominal syntax for diagrams. In: Coecke, B., Kissinger, A. (eds.) Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, EPTCS, Nijmegen, The Netherlands, 3–7 July 2017, vol. 266, pp. 71–83 (2017)MathSciNetCrossRef

24.

Yang, C., Vyatkin, V.: Transformation of Simulink models to IEC 61499 function blocks for verification of distributed control systems. Control Eng. Pract. 20(12), 1259–1269 (2012)CrossRef

25.

Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: 8th European Congress on ERTS 2016: Embedded Real Time Software and Systems, Toulouse, France, January 2016. SEE

26.

Lúcio, L., et al.: Model transformation intents and their properties. Softw. Syst. Model. 15(3), 647–684 (2016)CrossRef

27.

Malik, S.: Analysis of cyclic combinational circuits. IEEE Trans. Comput.-Aided Des. 13(7), 950–956 (1994)CrossRef

28.

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

29.

Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating Simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Heidelberg (2006). https://doi.org/10.1007/11901433_33CrossRef

30.

Minopoli, S., Frehse, G.: SL2SX translator: from Simulink to SpaceEx models. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 93–98. ACM, New York (2016)

31.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9CrossRefMATH

32.

Preoteasa, V., Dragomir, I., Tripakis, S.: Mechanically proving determinacy of hierarchical block diagram translations. CoRR, abs/1611.01337 (2018)

33.

Preoteasa, V., Tripakis, S.: Towards compositional feedback in non-deterministic and non-input-receptive systems. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 768–777. ACM, New York (2016)

34.

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

35.

Ryabtsev, M., Strichman, O.: Translation validation: from Simulink to C. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 696–701. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_57CrossRef

36.

Schlesinger, S., Herber, P., Göthel, T., Glesner, S.: Proving transformation correctness of refactorings for discrete and continuous Simulink models. In: ICONS 2016, The Eleventh International Conference on Systems, EMBEDDED 2016, International Symposium on Advances in Embedded Systems and Applications, pp. 45–50. IARIA XPS Press (2016)

37.

Schmeck, H.: Algebraic characterization of reducible flowcharts. J. Comput. Syst. Sci. 27(2), 165–199 (1983)MathSciNetCrossRef

38.

Selinger, P.: A survey of graphical languages for Monoidal categories. In: Coecke, B. (ed.) New Structures for Physics. LNP, vol. 813, pp. 289–355. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-12821-9_4CrossRefMATH

39.

Sfyrla, V., Tsiligiannis, G., Safaka, I., Bozga, M., Sifakis, J.: Compositional translation of Simulink models into synchronous BIP. In: SIES, pp. 217–220, July 2010

40.

The Coq Development Team: The Coq proof assistant reference. INRIA, 2016. Version 8.5 (2016)

41.

Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embed. Comput. Syst. 4(4), 779–818 (2005)CrossRef

42.

Zanasi, F.: Interacting Hopf algebras - the theory of linear systems. (Interacting Hopf Algebras - la théorie des systèmes linéaires). Ph.D. thesis, École normale supérieure de Lyon, France (2015)

43.

Zhou, C., Kumar, R.: Semantic translation of Simulink diagrams to input/output extended finite automata. Discret. Event Dyn. Syst. 22(2), 223–247 (2012)MathSciNetCrossRef

44.

Zou, L., Zhany, N., Wang, S., Franzle, M., Qin, S.: Verifying Simulink diagrams via a hybrid Hoare logic prover. In: EMSOFT, pp. 9:1–9:10, September 2013

Titel: Mechanically Proving Determinacy of Hierarchical Block Diagram Translations
verfasst von: Viorel Preoteasa
Iulia Dragomir
Stavros Tripakis
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-11244-8

Electronic ISBN: 978-3-030-11245-5

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-11245-5_27

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"