Advertisement

Mechanically Proving Determinacy of Hierarchical Block Diagram Translations

  • Viorel PreoteasaEmail author
  • Iulia DragomirEmail author
  • Stavros TripakisEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)

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.

Notes

Acknowledgments

We would like to thank Gheorghe Ştefănescu for his help with the algebra of flownomials.

References

  1. 1.
    Rahim, L.A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003–1028 (2015)CrossRefGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Amrani, M., et al.: Formal verification techniques for model transformations: a tridimensional classification. J. Object Technol. 14(3), 1:1–43 (2015)CrossRefGoogle Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998).  https://doi.org/10.1007/978-1-4612-1674-2CrossRefzbMATHGoogle Scholar
  6. 6.
    Baez, J.C., Erbele, J.: Categories in control. CoRR, abs/1405.6881 (2015)Google Scholar
  7. 7.
    Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123–153 (2014)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Berry, G.: The constructive semantics of pure Esterel (1999)Google Scholar
  9. 9.
    Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. SIGPLAN Not. 47(5), 129–138 (2012)Google Scholar
  10. 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)CrossRefGoogle Scholar
  11. 11.
    Calegari, D., Szasz, N.: Verification of model transformations. Electron. Notes Theor. Comput. Sci. 292, 5–25 (2013)CrossRefGoogle Scholar
  12. 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)CrossRefGoogle Scholar
  13. 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_49CrossRefGoogle Scholar
  14. 14.
    Ştefănescu, G.: Network Algebra. Springer, London (2000).  https://doi.org/10.1007/978-1-4471-0479-7CrossRefzbMATHGoogle Scholar
  15. 15.
    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)MathSciNetCrossRefGoogle Scholar
  16. 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_3CrossRefGoogle Scholar
  17. 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_12CrossRefGoogle Scholar
  18. 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. 19.
    Eclipse: ATL - a model transformation technology. http://www.eclipse.org/atl/
  20. 20.
    Edwards, S., Lee, E.A.: The semantics and execution of a synchronous block-diagram language. Sci. Comput. Prog. 48, 21–42(22) (2003)MathSciNetCrossRefGoogle Scholar
  21. 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)Google Scholar
  22. 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)Google Scholar
  23. 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)MathSciNetCrossRefGoogle Scholar
  24. 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)CrossRefGoogle Scholar
  25. 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. SEEGoogle Scholar
  26. 26.
    Lúcio, L., et al.: Model transformation intents and their properties. Softw. Syst. Model. 15(3), 647–684 (2016)CrossRefGoogle Scholar
  27. 27.
    Malik, S.: Analysis of cyclic combinational circuits. IEEE Trans. Comput.-Aided Des. 13(7), 950–956 (1994)CrossRefGoogle Scholar
  28. 28.
  29. 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_33CrossRefGoogle Scholar
  30. 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)Google Scholar
  31. 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-9CrossRefzbMATHGoogle Scholar
  32. 32.
    Preoteasa, V., Dragomir, I., Tripakis, S.: Mechanically proving determinacy of hierarchical block diagram translations. CoRR, abs/1611.01337 (2018)Google Scholar
  33. 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)Google Scholar
  34. 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_14CrossRefGoogle Scholar
  35. 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_57CrossRefGoogle Scholar
  36. 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)Google Scholar
  37. 37.
    Schmeck, H.: Algebraic characterization of reducible flowcharts. J. Comput. Syst. Sci. 27(2), 165–199 (1983)MathSciNetCrossRefGoogle Scholar
  38. 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_4CrossRefzbMATHGoogle Scholar
  39. 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 2010Google Scholar
  40. 40.
    The Coq Development Team: The Coq proof assistant reference. INRIA, 2016. Version 8.5 (2016)Google Scholar
  41. 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)CrossRefGoogle Scholar
  42. 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)Google Scholar
  43. 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)MathSciNetCrossRefGoogle Scholar
  44. 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 2013Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Space Systems FinlandEspooFinland
  2. 2.Univ. Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAGGrenobleFrance
  3. 3.Aalto UniversityEspooFinland
  4. 4.Northeastern UniversityBostonUSA

Personalised recommendations