Abstract

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.

-- Daniel Amyot - 05 Jan 2010

Discussion

• Paper available at http://dx.doi.org/10.1109/ACIIDS.2009.66 or from the authors ({thuantn,thuongttm,khanhtv,hanv}@vnu.edu.vn)