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 events paths will be checked with the order of events of PSMs by the proposed algorithm. © 2009 IEEE.

Truong N.T., Tran T.M.T., To V.K., Nguyen V.H.

286.pdf    Gửi cho bạn bè

Từ khóa : B method; Component model; Component-based software engineering; Design phase; Expression problem; Expressive power; Graph-based; Graph-based methods; Parallel processing; State machine; Use case maps; Algorithms; Model checking; Models; Object oriented programming; Semiconductor quantum dots; Sequential switching; Software engineering; Database systems