Space Effective Model Checking for Component-Interaction Automata

Nikola Beneš, Milan KřiváNek & Filip ŠTefaňáK
The techniques of component-based development are becoming a common practice in the area of software engineering. One of the crucial issues in the correctness of such systems is the correct interaction among the components. The formalism of component-interaction automata was devised to model various aspects of such interaction, as well as to allow automated verification in the form of model checking with properties expressed in the component-interaction LTL, a variant of the known linear temporal...