6533b831fe1ef96bd129981b

RESEARCH PRODUCT

ATL model checking in the cloud

Laura Florentina StoicaFlorin Stoica

subject

Model checkingSQLProgramming languagebusiness.industrySemantics (computer science)Computer scienceInteractive designCloud computingcomputer.software_genreTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESOperating systemAlgorithm designWeb servicebusinesscomputercomputer.programming_languageGraphical user interface

description

This paper gives an overview of our recent work on implementing a new interactive ATL model checker for verification of open systems. In verification based on model checking, we need to provide a model of the system and also write down the properties (ATL formulas) that we require the system to satisfy. Traditionally, the semantics of ATL is given in terms of concurrent game structures. 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. The server part, published as Web service in OpenShift cloud platform, embeds the core of the ATL model checker, and the client provides an intuitive graphical interface for interactive design of ATL models. Our original implementation of the model checking algorithm is based on SQL queries. Several APIs are available for programmatic construction of large models.

yearjournalcountryeditionlanguage
2015-09-012015 Internet Technologies and Applications (ITA)
https://doi.org/10.1109/itecha.2015.7317394