A uniform framework for modeling and verifying components and connectors

Christel BaierChristel Baier, Tobias BlechmannTobias Blechmann, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz

DOI Link

Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Klüppelholz
A uniform framework for modeling and verifying components and connectors
Proc. of the 11th International Conference on Coordination Models and Languages (COORD), volume 5521 of Lecture Notes in Computer Science, 247--267, 2009. Springer

Details
Bibtex

KurzfassungAbstract
The purpose of this paper is to present a framework to model component interfaces and the component connectors that provide the glue code for the components. Our modeling approach is based on two input languages which rely on the same automata model. One of them is a scripting language which can serve to specify exogenous or endogenous coordination mechanisms. The other one is a guarded command language which has been designed to specify behavioral component interfaces, but can also be used to design component connectors. This hybrid approach allows nesting of the two specification languages, supports compositional design, modular verification and reusability of components or component connectors. It yields the input language of our verification toolset Vereofy which realizes several model checking algorithms for components, component connectors, and the composite system.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-02053-7_13.

@inproceedings{BBKK2009,
  author    = {Christel Baier and Tobias Blechmann and Joachim Klein and Sascha
               Kl{\"{u}}ppelholz},
  title     = {A uniform framework for modeling and verifying components and
               connectors},
  booktitle = {Proc. of the 11th International Conference on Coordination Models
               and Languages (COORD)},
  series    = {Lecture Notes in Computer Science},
  volume    = {5521},
  publisher = {Springer},
  year      = {2009},
  pages     = {247--267},
  doi       = {10.1007/978-3-642-02053-7_13}
}