EXPLORE PUBLICATIONS BY COUNTRIES

ATL, Model Checking, Web Services, Relational Algebra, SQL.

In this paper we present a new ATL model checking tool used for verification of open systems. An open system interacts with its environment and its behavior depends on the state of the system as well as the behavior of the environment. The Alternating-Time Temporal Logic (ATL) logic is interpreted over concurrent game structures, considered as natural models for compositions of open systems. In contrast to previous approaches, our tool permits an interactive design of the ATL models as state-transition graphs, and is based on client/server architecture: ATL Designer, the client tool, allows an interactive construction of the concurrent game structures as a directed multi-graphs and the ATL Checker, the core of our tool, represents the server part and is published as Web service. The ATL Checker includes an algebraic compiler which was implemented using ANTLR (Another Tool for Language Recognition). Our model checker tool allows designers to automatically verify that systems satisfy specifications expressed by ATL formulas. The original implementation of the model checking algorithm is based on Relational Algebra expressions translated into SQL queries. Several database systems were used for evaluating the system performance in verification of large ATL models.