Causal semantics for the algebra of connectors.

*(English)*Zbl 1207.68203Summary: The Algebra of Connectors \(\mathcal{AC}(P)\) is used to model structured interactions in the BIP component framework. Its terms are connectors, relations describing synchronization constraints between the ports of component-based systems. Connectors are structured combinations of two basic synchronization protocols between ports: rendezvous and broadcast.

In a previous paper, we have studied interaction semantics for \(\mathcal{AC}(P)\) which defines the meaning of connectors as sets of interactions. This semantics reduces broadcasts into the set of their possible interactions and thus blurs the distinction between rendezvous and broadcast. It leads to exponentially complex models that cannot be a basis for efficient implementation. Furthermore, the induced semantic equivalence is not a congruence.

For a subset of \(\mathcal{AC}(P)\), we propose a new \(causal\) semantics that does not reduce broadcast into a set of rendezvous and explicitly models the causal dependency relation between ports. The Algebra of Causal Interaction Trees \(\mathcal{T}(P)\) formalizes this subset. It is the set of the terms generated from interactions on the set of ports \(P\), by using two operators: a causality operator and a parallel composition operator. Terms are sets of trees where the successor relation represents causal dependency between interactions: an interaction can participate in a global interaction only if its father participates too. We show that causal semantics is consistent with interaction semantics; the semantic equivalence on \(\mathcal{T}(P)\) is a congruence. Furthermore, it defines an isomorphism between \(\mathcal{T}(P)\) and a subset of \(\mathcal{AC}(P)\).

Finally, we define for causal interaction trees a boolean representation in terms of causal rules. This representation is used for their manipulation and simplification as well as for synthesizing connectors.

In a previous paper, we have studied interaction semantics for \(\mathcal{AC}(P)\) which defines the meaning of connectors as sets of interactions. This semantics reduces broadcasts into the set of their possible interactions and thus blurs the distinction between rendezvous and broadcast. It leads to exponentially complex models that cannot be a basis for efficient implementation. Furthermore, the induced semantic equivalence is not a congruence.

For a subset of \(\mathcal{AC}(P)\), we propose a new \(causal\) semantics that does not reduce broadcast into a set of rendezvous and explicitly models the causal dependency relation between ports. The Algebra of Causal Interaction Trees \(\mathcal{T}(P)\) formalizes this subset. It is the set of the terms generated from interactions on the set of ports \(P\), by using two operators: a causality operator and a parallel composition operator. Terms are sets of trees where the successor relation represents causal dependency between interactions: an interaction can participate in a global interaction only if its father participates too. We show that causal semantics is consistent with interaction semantics; the semantic equivalence on \(\mathcal{T}(P)\) is a congruence. Furthermore, it defines an isomorphism between \(\mathcal{T}(P)\) and a subset of \(\mathcal{AC}(P)\).

Finally, we define for causal interaction trees a boolean representation in terms of causal rules. This representation is used for their manipulation and simplification as well as for synthesizing connectors.

##### MSC:

68Q55 | Semantics in the theory of computing |

##### Keywords:

BIP; component; connectors; connector synthesis; interaction; causal semantics; causal interaction trees
PDF
BibTeX
Cite

\textit{S. Bliudze} and \textit{J. Sifakis}, Form. Methods Syst. Des. 36, No. 2, 167--194 (2010; Zbl 1207.68203)

Full Text:
DOI

##### References:

[1] | Arbab F (2004) Reo: a channel-based coordination model for component composition. Math Struct Comput Sci 14(3):329–366 · Zbl 1085.68552 |

[2] | Arbab F, Meng S (2008) Synthesis of connectors from scenario-based interaction specifications. In: CBSE’08. LNCS, vol 5282. Springer, Berlin, pp 114–129 |

[3] | Balarin F, Watanabe Y, Hsieh H, Lavagno L, Passerone C, Sangiovanni-Vincentelli A (2003) Metropolis: an integrated electronic system design environment. IEEE Comput 36(4):45–52 |

[4] | Balasubramanian K, Gokhale A, Karsai G, Sztipanovits J, Neema S (2006) Developing applications using model-driven design environments. IEEE Comput 39(2):33–40 |

[5] | Basu A, Bozga M, Sifakis J (2006) Modeling heterogeneous real-time components in BIP. In: 4th IEEE international conference on software engineering and formal methods (SEFM06), September 2006, pp 3–12. Invited talk |

[6] | Benveniste A, Guernic PL, Jacquemot C (1991) Synchronous programming with events and relations: the SIGNAL language and its semantics. Sci Comput Program 16(2):103–149 · Zbl 0745.68031 |

[7] | Bernardo M, Ciancarini P, Donatiello L (2000) On the formalization of architectural types with process algebras. In: SIGSOFT FSE, pp 140–148 |

[8] | BIP. http://www-verimag.imag.fr/\(\sim\)async/BIP/bip.html |

[9] | Bliudze S, Sifakis J (2007) The algebra of connectors–structuring interaction in BIP. In: Proceedings of the EMSOFT’07, pp 11–20. ACM SigBED, October 2007 · Zbl 1390.68031 |

[10] | Bliudze S, Sifakis J (2008) The algebra of connectors–structuring interaction in BIP. IEEE Trans Comput 57(10):1315–1330 |

[11] | Bliudze S, Sifakis J (2008) A notion of glue expressiveness for component-based systems. In: van Breugel F, Chechik M (eds) CONCUR 2008. LNCS, vol 5201. Springer, Berlin, pp 508–522 · Zbl 1160.68458 |

[12] | Bruni R, Lanese I, Montanari U (2006) A basic algebra of stateless connectors. Theor Comput Sci 366(1):98–120 · Zbl 1153.68331 |

[13] | Darondeau P, Degano P (1989) Causal trees. In: Ausiello G, Dezani-Ciancaglini M, Rocca SRD (eds) ICALP. LNCS, vol 372. Springer, Berlin, pp 234–248 |

[14] | Eker J, Janneck J, Lee E, Liu J, Liu X, Ludvig J, Neuendorffer S, Sachs S, Xiong Y (2003) Taming heterogeneity: the Ptolemy approach. Proc IEEE 91(1):127–144 |

[15] | Fiadeiro JL (2004) Categories for software engineering. Springer, Berlin |

[16] | Galik O, Bureš T (2005) Generating connectors for heterogeneous deployment. In: SEM’05. ACM, New York, pp 54–61 |

[17] | Halbwachs N, Caspi P, Raymond P, Pilaud D (1991) The synchronous dataflow programming language lustre. Proc IEEE 79:1305–1320 |

[18] | Hoare CAR (1985) Communicating sequential processes. Prentice Hall international series in computer science. Prentice Hall, New York |

[19] | Inverardi P, Tivoli M (2001) Automatic synthesis of deadlock free connectors for com/dcom applications. In: ACM proceedings of the joint 8th ESEC and 9th FSE, Vienna, September 2001. ACM, New York |

[20] | Maggiolo-Schettini A, Peron A, Tini S (2003) A comparison of Statecharts step semantics. Theor Comput Sci 290(1):465–498 · Zbl 1018.68045 |

[21] | Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification, vol 1. Springer, New York · Zbl 0753.68003 |

[22] | Maraninchi F, Rémond Y (2001) Argos: an automaton-based synchronous language. Comput Lang 27:61–92 · Zbl 1050.68020 |

[23] | Milner R (1989) Communication and concurrency. Prentice Hall international series in computer science. Prentice Hall, New York |

[24] | Nowak D (2006) Synchronous structures. Inf Comput 204(8):1295–1324 · Zbl 1110.68019 |

[25] | Ray A, Cleaveland R (2003) Architectural interaction diagrams: AIDs for system modeling. In: ICSE’03: proceedings of the 25th international conference on software engineering. IEEE Computer Society, Washington, pp 396–406 |

[26] | Sifakis J (2005) A framework for component-based construction. In: 3rd IEEE international conference on software engineering and formal methods (SEFM05), September 2005, pp 293–300. Keynote talk |

[27] | Spitznagel B, Garlan D (2003) A compositional formalization of connector wrappers. In: ICSE. IEEE Computer Society, Los Alamitos, pp 374–384 |

[28] | Stefănescu G (2000) Network algebra. Springer, New York · Zbl 0956.68002 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.