A Technique to Check the Implementability of Behavioral Specifications with Frameworks

In software development with frameworks, it is essential to use the framework with which given software requirements are implementable. This paper focuses on use cases as the requirements specifications and proposes a technique to check whether the given use cases are implementable with the framework. To check the implementability, consistency of branch conditions of the frameworks and the requirements specification has to be checked as well as equivalence of action sequences between the frameworks and the requirements specification. To this end, a novel approach based on a satisfiability problem for deriving the consistent truth assignments of the branch conditions is introduced. The approach can be incorporated in bi-simulation checking for assuring the equivalence of the action sequences, and therefore, the implementability can be checked. Furthermore, this paper shows a feasibility of the proposed technique by using Compositional Reachability Analysis as a mean of bi-simulation checking.