|
The Influence of Software Module Systems on Modular Verification, H. Li (Brown University), K. Fisler (Worcester Polytechnic Institute) and S. Krishnamurthi (Brown University). Proceedings of the 9th SPIN Workshop Grenoble, France.
Collaborations are modules that encapsulate code involved in the same operation ina system. They have received increasing attention in software engineering because their separation of behavior simplifies software evolution, configuration, and maintenance. This paper explores the effect of these designs on modular model checking, especiallyon state space sizes and on the need for property decomposition.
Model checking is an attractive technique for verification which is increasingly used in the field of hardware design. Alas, applying model checking to software is problematic beacuse of the so called state explosion problem. Algorithms for model checking are based on the (efficient) exploration of the entire state space of the model, to see that it satisfies the temporal logic properties which serve as the specification. Software systems tend to have a much larger state space than hardware devices, and thus model checkers have a hard time working with them. Modular model checking may help in solving this problem.
This paper presents one approach. Buzzwords: PLT Scheme is mentioned (of course), and the SPIN model checker.
Posted to Software-Eng by Ehud Lamm on 7/7/02; 10:31:22 AM
|
Influence of Software Module Systems on Modular Verification
