-
- Kathi Fisler
- Department of Computer Science, Worcester Polytechnic Institute, Worcester, MA,
-
- Shriram Krishnamurthi
- Computer Science Department, Brown University, Providence, RI,
説明
<jats:p>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.</jats:p>
収録刊行物
-
- ACM SIGSOFT Software Engineering Notes
-
ACM SIGSOFT Software Engineering Notes 26 (5), 152-163, 2001-09
Association for Computing Machinery (ACM)