Modular verification of collaboration-based software designs. - Fisler, Kathi
Most existing modular model checking techniques betray their hardware roots: they assume that modules compose in parallel. In contrast, collaboration-based software designs, which have proven very successful in several domains, are sequential in the simplest case. Most interesting collaboration-based designs are really quasi-sequential compositions of parallel compositions. These designs demand and inspire new verification techniques. This paper presents algorithms that exploit the software's modular decomposition to verify collaboration-based designs. Our technique can verify most properties locally in the collaborations; we also characterize when a global state space construction is unavoidable. We have validated our proposal by testing it on several designs.
Keywords: Software; Software engineering; Software / Program Verification; Model checking; Software architectures; Languages (e.g., description, interconnection, definition).; Design tools and techniques; Modules and interfaces; Theory of computation; Logics and meanings of programs; Specifying and Verifying and Reasoning about Programs; Specification techniques; Design; Verification; Aspect oriented programming; Collaboration based design; Compositional reasoning; Computer-aided verification; Model checking; Software architecture