Model Checking the Component-based Protocol Specification for Proving the Design Correctness

We developed a component-oriented modeling approach for the design of communication protocols and distributed systems. The approach aims at the reuse of components represented by means of Unified Modeling Language (UML) diagrams. Designs based on compositions of components have to formally be proved for correctness. In this paper we propose a verification approach by combining trace equivalence and model checking to verify UML-based designs of communication protocols. Our method consists of two steps. Foremost, the internal and external component behaviors are verified independently regarding their formal correctness. Thereafter the correctness and consistency of compositions is 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 designs into PROMELA. We evaluate our approach for an example data transfer protocol as a case study.