00000cab a22000003a 4500 UP-99796217608835910 Buklod 20231007234832.0 m |o d | ta 090525s xx d | ||r ||||| || DENGII eng Fisler, Kathi Modular verification of collaboration-based software designs. pp. 152-163 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. 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. Software engineering notes. 26, 5 (2001). FO UPD DENG-II Article