An approach to verify component-based designs

Ensuring design correctness is an important task in the software development and in particular component-based protocol development. We developed a component-oriented design approach for the design of communication protocols and distributed systems. The approach aims at the reuse of components represented by Unified Modeling Language (UML) diagrams. In this paper we propose a verification approach to verify our component-based protocol designs by combing trace equivalence and model checking. Foremost, the internal and external component behaviors are verified independently regarding their formal correctness. Next, the correctness and consistency of compositions are verified. This is achieved by generating the component adaptation path as traces during the composition. The requirements, i.e., safety and liveness properties, are formulated using linear temporal logic formulae. We apply the Spin tool as our model checking mechanism. For this, we present a method for automatically transforming the protocol design components into PROMELA.