Model checking is nowadays being used as advanced technique to analyse, design and debug reactive systems. This paper gives an overview of our recent work on implementing a new interactive CTL model checker. In contrast to previous approaches, our tool permits an interactive design of the CTL models as state-transition graphs, and is based on client/server architecture. The server part embeds the core of the CTL model checker and is published as a Web service. A C# client provides an intuitive graphical interface for interactive design of CTL models. Java and C# APIs are available for programmatic construction of large models. Experimental results are encouraging, showing that our tool is able to handle large systems efficiently.
展开▼
