Towards a sound modular model checking of collaboration-based software designs

Collaboration-based designs [K. Fisler et al. (2001), T. T. Nguyen et al. (2003), Y. Smaragdakis et al. (1998)] are an effective software development approach due to its achievement in separation of concerns [G. Kiczales et al., (1997), P. Tarr et al. (1999)]. These designs also demand a new model checking technique allowing to prove system correctness by verifying each collaboration individually with a minimum assumption about other collaborations. To verify a collaboration of multiple actors, a typical technique consists of constructing a standard cross-product of actor statecharts as global state space and then checking properties with respect to that global space. We initially point out some drawbacks of a previous approach [K. Fisler et al. (2001)] in verifying collaboration. Then, in addition to intra-object behaviors in statecharts as of [K. Fisler et al. (2001)], we first improve the technique by imposing additional constraints to model checking process via protocol invariants which are essentially inter-object behaviors. Due to these additional constraints, state space is reduced and more importantly, our model reflects more accurately about system behavior by eliminating those unreachable states. Second, a more general form, i.e. multiple exit and re-entry states, of the interface between two collaborations is used instead of a fixed interface with single exit and re-entry states. Some pre-processing work on reentry states and solutions to specifics of properties to be verified are also discussed regarding to the soundness of the verification algorithm.