TY - GEN
T1 - The algebra of connectors
T2 - EMSOFT'07: 7th ACM and IEEE International Conference on Embedded Software
AU - Bliudze, Simon
AU - Sifakis, Joseph
PY - 2007/12/1
Y1 - 2007/12/1
N2 - We provide an algebraic formalisation of connectors in BIP. These are used to structure interactions in a component-based system. A connector relates a set of typed ports. Types are used to describe different modes of synchronisation: rendezvous and broadcast, in particular. Connectors on a set of ports P are modelled as terms of the algebra AC(P), generated from P by using a binary fusion operator and a unary typing operator. Typing associates with terms (ports or connectors) synchronisation types - trigger or synchron - , which determine modes of synchronisation. Broadcast interactions are initiated by triggers. Rendezvous is a maximal interaction of a connector including only synchrons. The semantics of AC(P) associates with a connector the set of its interactions. It induces on connectors an equivalence relation which is not a congruence as it is not stable for fusion. We provide a number of properties of AC(P) used to symbolically simplify and handle connectors. We provide examples illustrating applications of AC(P), including a general component model encompassing synchrony, methods for incremental model decomposition, and efficient implementation by using symbolic techniques.
AB - We provide an algebraic formalisation of connectors in BIP. These are used to structure interactions in a component-based system. A connector relates a set of typed ports. Types are used to describe different modes of synchronisation: rendezvous and broadcast, in particular. Connectors on a set of ports P are modelled as terms of the algebra AC(P), generated from P by using a binary fusion operator and a unary typing operator. Typing associates with terms (ports or connectors) synchronisation types - trigger or synchron - , which determine modes of synchronisation. Broadcast interactions are initiated by triggers. Rendezvous is a maximal interaction of a connector including only synchrons. The semantics of AC(P) associates with a connector the set of its interactions. It induces on connectors an equivalence relation which is not a congruence as it is not stable for fusion. We provide a number of properties of AC(P) used to symbolically simplify and handle connectors. We provide examples illustrating applications of AC(P), including a general component model encompassing synchrony, methods for incremental model decomposition, and efficient implementation by using symbolic techniques.
KW - Design
KW - Theory
U2 - 10.1145/1289927.1289935
DO - 10.1145/1289927.1289935
M3 - Conference contribution
AN - SCOPUS:38549107072
SN - 9781595938251
T3 - EMSOFT'07: Proceedings of the Seventh ACM and IEEE International Conference on Embedded Software
SP - 11
EP - 20
BT - EMSOFT'07
Y2 - 30 September 2007 through 3 October 2007
ER -