Brief announcement: incremental component-based modeling, verification, and performance evaluation of distributed reset
In this work, we apply a methodology which consistently integrates modeling, verification, and performance evaluation techniques, based on the BIP (Behavior, Interaction, Priority) component framework developed at Verimag [A. Basu et al., 2006; A. Basu et al., 2008]. BIP is based on a semantic model encompassing composition of heterogeneous components. The distributed semantics of BIP allows generating from a high-level component-based model in BIP an observationally equivalent distributed implementation [A. Basu et al., 2008]. BIP uses two families of composition operators for expressing coordination between components: interactions and priorities. Interactions may involve multiple components (unlike traditional point-to-point formalisms) and are expressed by combining two protocols: rendezvous and broadcast. We note that addition of interactions among components adds no extra behaviors.