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 (open access version) 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. Our work builds upon the Refinement Calculus of Reactive Systems (RCRS), a publicly available compositional framework for modeling and reasoning about reactive systems

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.

The main contributions of this work are then the following:

  1. We formally and mechanically define a translation algorithm for HBDs.
  2. We prove that despite its internal nondeterminism, the algorithm achieves deterministic results in the sense that all possible algebra terms that can be generated by the different non-deterministic choices are semantically equivalent.
  3. We formalize two translation strategies introduced in [] as refinements of the abstract algorithm.
  4. We formalize also the third strategy (feedbackless) introduced in [] as an independent algorithm.
  5. We mechanically prove the equivalence of these three translation strategies.
  6. We make our results publicly available at https://github.com/hbd-translation/TranslateHBD.

Moreover, we believe that our results are reusable in other contexts as well, in at least two ways. First, every other translation that can be shown to be a refinement/special case of our abstract translation algorithm, is automatically correct.  Second, our algorithms translate diagrams into an abstract algebra. By choosing different models of this algebra we obtain translations into these alternative models.

As future work, we plan to investigate further HBD translation strategies, in addition to those studied above. Currently, the RCRS Translator can only partially handle diagrams with algebraic loops, i.e., with instantaneous circular dependencies. Fully dealing with diagrams with algebraic loops is a non-trivial problem, because of the subtleties of instantaneous feedback for non-deterministic and non-input-receptive systems []. For deterministic and input-receptive systems, however, the model of constructive functions should be sufficient.

[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_3

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

 

Share This