Checking the Consistency between UCM and PSM Using a Graph-Based Method

Checking the consistency in component models at design phase is essential in component-based software engineering (CBSE). In our previous work, we proposed an approach for verifying automatically the matching between protocol state machines (PSMs) and the use case map (UCM), using the B method. Due to the expressive power of B notations, however, we cannot describe the parallel processing in the implementation machine, particularly we are not able to express all features (such as AND-forks/joins, OR-forks/joins) of UCMs in a B implementation machine. In this work, we propose an approach to solve the expression problem of UCM features using a graph-based algorithm. The UCM path which describes the interaction between components is extracted and then decomposed into sequential events´ paths if it has AND-forks/joins and/or OR-forks/joins. Each of sequential eventspsila paths will be checked with the order of events of PSMs by the proposed algorithm.