A New Model Checking Tool

摘要

In this paper we present a new CTL model checking tool used to prove whether a CTL model represented as a directed graph satisfies a set of specifications given in form of one or more temporal logic formulas. Our tool is implemented in client-server paradigm: CTL Designer, the client tool, allows an interactive construction of the Kripke model as a directed graph and the CTL Checker, the core of our tool, represents the server part and is published as Web service. The CTL Checker includes an algebraic compiler implemented with ANTLR (Another Tool for Language Recognition) support. The main function of the Web service is to parse a given formula, find the set of nodes in which the formula is satisfied and return result to the user. As test case for our tool, we choose a CTL Model for Login Page Controller. The model will check if logging is allowed or not depending on input data.