Automata Based Model Checking for Reo Connectors

Reo is a connector language for the exogenous composition and orchestration of components in a software system. An operational semantics of Reo connectors can be given in terms of Buchi automata over a suitable alphabet of records, capturing both synchronization and context dependency requirements. In this paper, we define an action based linear time temporal logic for expressing properties of Reo connectors. Formulas can be synthesized into Buchi automata representing Reo connectors, thus leading to an automata based model checking algorithm. By generalizing standard automata based model checking algorithms for linear time temporal logic, we give an efficient on-the-fly algorithm for the model checking of formulas for Reo connectors.