6533b836fe1ef96bd12a088a

RESEARCH PRODUCT

Implementing an ATL model checker tool using relational algebra concepts

Florin StoicaLaura Florentina Stoica

subject

Model checkingSQLTheoretical computer scienceProgramming languageComputer sciencecomputer.internet_protocolRelational algebracomputer.software_genreOpen system (systems theory)Temporal logicWeb servicecomputerServer-sideXMLcomputer.programming_language

description

Alternating-Time Temporal Logic (ATL) is a branching-time temporal logic that naturally describes computations 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. ATL model-checking is a well-established technique for verifying that a formal model representing such a system satisfies a given property. In this paper we describe a new interactive model checker environment based on algebraic approach. Our tool is implemented in client-server paradigm. The client part allows an interactive construction of ATL models represented by concurrent game structures as directed multi-graphs. The server part embeds an ATL model checking algorithm implemented using ANTLR and Relational Algebra expressions translated into SQL queries. The server side of our tool was published as a Web service exposing its functionality to various clients through standard XML interfaces.

yearjournalcountryeditionlanguage
2014-09-012014 22nd International Conference on Software, Telecommunications and Computer Networks (SoftCOM)
https://doi.org/10.1109/softcom.2014.7039096