Modeling synchronous systems in BIP

ABSTRACT

We present a general approach for modeling synchronous component-based systems. These are systems of synchronous components strongly synchronized by a common action that initiates steps of each component. We propose a general model for synchronous systems. Steps are described by acyclic Petri nets equipped with data and priorities. Petri nets are used to model concurrent flow of computation. Priorities are instrumental for enforcing run-to-completion in the execution of a step.

We study a class of well-triggered synchronous systems which are by construction deadlock-free and their computation within a step is confluent. For this class, the behavior of components is modeled by modal flow graphs. These are acyclic graphs representing three different types of dependency between two events p and q: strong dependency (p must follow q), weak dependency (p may follow q), conditional dependency (if both p and q occur then p must follow q).

We propose a translation of Lustre into well-triggered synchronous systems. This translation is modular and exhibits not only data-flow connections between nodes but also their synchronization by using clocks.

References

1. A. Basu, M. Bozga, and J. Sifakis. Modeling heterogeneous real-time systems in BIP. In Proceedings of SEFM'06, pages 3--12. invited talk.
2. A. Benveniste, B. Caillaud, L. P. Carloni, P. Caspi, and A. L. Sangiovanni-Vincentelli. Composing heterogeneous reactive systems. ACM-TECS, 7(4), 2008.
3. S. Bliudze and J. Sifakis. A notion of glue expressiveness for component-based systems. In Proceedings of CONCUR'08, LNCS 5201, pages 508--522, 2008.
4. M. Bozga, M. Jaber, and J. Sifakis. Source-to-source architecture transformation for performance optimization in BIP. In IEEE Symposium on Industrial Embedded Systems (SIES'09), 2009.
5. M. Bozga, V. Sfyrla, and J. Sifakis. Modeling synchronous systems in BIP. Technical Report TR-2009-8, Verimag.
6. S. L. Campbell, J.-P. Chancelier, and R. Nikoukhah. Modeling and Simulation in Scilab/Scicos. Springer.
7. P. Combes, D. Harel, and H. Kugler. Modeling and verification of a telecommunication application using live sequence charts and the play-engine tool. In Proceedings of ATVA'05, LNCS 3707, pages 414--428.
8. F. Commoner, A. W. Holt, S. Even, and A. Pnueli. Marked directed graphs. Computer System Sciences, 5(5):511--523, 1971.
9. J. Eker, J. W. Janneck, E. A. Lee, J. Liu, X. Liu, J. Ludvig, S. Neuendorffer, S. Sachs, and Y. Xiong. Taming heterogeneity - the Ptolemy approach. Proceedings of IEEE, 91(1):127--144, 2003.
10. P. L. Guernic, T. Gautier, M. L. Borgne, and C. L. Maire. Programming real time applications with Signal. Proceedings of IEEE, 79(9):1321--1336, 1991.
11. N. Halbwachs. About synchronous programming and abstract interpretation. SCP, 31(1):75--89, 1998.
12. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of IEEE, 79(9):1305--1320, 1991.
13. D. Harel and S. Maoz. Assert and negate revisited: Modal semantics for UML sequence diagrams. Software and System Modeling, 7(2):237--252, 2008.
14. K. G. Larsen, U. Nyman, and A. Wasowski. Modal i/o automata for interface and product line theories. In Proceedings of ESOP'07, LNCS 4421, pages 64--79.
15. F. Maraninchi and T. Bouhadiba. 42: Programmable models of computation for a component-based approach to heterogeneous embedded systems. In Proceedings of ACM-GPCE'07.
16. D. Nowak. Synchronous structures. Information and Computation, 204(8):1295--1324, 2006.
17. Y. Zhou and E. A. Lee. Causality interfaces for actor networks. ACM-TECS, 7(3), 2008.

Index Terms

• Computing methodologies

  • Concurrent computing methodologies

    • Concurrent programming languages

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Concurrent programming languages

• Theory of computation

  • Logic

  • Models of computation

  • Semantics and reasoning

    • Program reasoning