Checking interaction consistency in MARMOT component refinements

Abstract

The refinement process of component designs is one of the basic building blocks for systematic component-based development. In this process, identifying inconsistent specifications of interactions among refined and refining components can be a critical issue for system safety and/or reliability. To efficiently identify interaction inconsistencies, we have been developing a consistency checking framework integrated into the model-driven component-based development methodology MARMOT, using model checking as a debugging tool. We introduce our notion of interaction consistency, propose a general framework for integrating the consistency checking mechanism into the refinement process, and demonstrate how the efficiency of identifying inconsistencies can be improved through abstractions. © Springer-Verlag Berlin Heidelberg 2007.