A Comparison of Three Model Checkers Applied to a Distributed Database Problem

ct Increasingly, model checking is being applied to more abstract problem domains than the traditional protocol analysis. The extent to which such an approach is able to provide useful insight into the problem domain depends to a large degree on the nature of the tool used. This paper reports the results of a study using three di erent model checkers, which di er widely in their speci cation language, internal implementation, and facilities for specifying correctness properties. act model of an industrial distributed database application has been studied using the three tools. A detailed model of the application using each of the tools is presented, and the extent to which each tool allows us to investigate interesting properties of the problem domain is compared. Some conclusions are drawn regarding the usefulness of model checking at an abstract level and the importance of selecting a tool appropriate to the nature of the problem.

• Type: Conference
• Year: 2000
• Where: IWFM
• Authors: A. J. Currie
• Keywords: IWFM 2000, IWFM 2001, Model, Model Checking, Problem Domain