Scalability in Model Checking through Relational Databases

/ Database & Software Engineering, EU Research Publications, Journal Publications, Romania Research Publications / By

ABSTRACT

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 Alternatin…

 

See full abstracts, authors, references, citations & other publication information.

MORE INFORMATION >>.

+

…g-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.

See The Link

Full Text/Reference Website: https://www.cscjournals.org/library/manuscriptinfo.php?mc=IJLP-33

Scalability in Model Checking through Relational Databases
Scalability in Model Checking through Relational Databases

AUTHORS
Dr. Florin Stoica – Department of Mathematics and Computer Science, Lucian Blaga, University of Sibiu – Romania

KEYWORDS

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

Indexing Keywords: Scalability in Model Checking through Relational Databases, Scalability in Model Checking, Scalability in Relational Databases, Model Checking through Relational Databases, Model Checking, Relational Databases.

Pages: 1-22
Revised: 30-04-2016
Published: 01-06-2016

Published in International Journal of Logic and Computation (IJLP).

Volume: 4
Issue: 1
Publication Date: 01-06-2016

*Randomly selected references used in the publication “Scalability in Model Checking through Relational Databases”.

SEE THE LINK >>

  • W. Van der Hoek, M. Wooldridge. “Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications”. Studia Logica 75, Kluwer Academic Publishers, pp. 125-157 2003.
  • G. Holzmann. “The model checker SPIN”. IEEE Trans. on Software Engineering, vol. 23, pp. 279–295, 1997.
  • F. Lerda, N. Sinha, M. Theobald. “Symbolic Model Checking of Software”. Electronic Notes in Theoretical Computer Science, Volume 89, Issue 3, pp. 480–498, 2003.
  • A.J. Hu. “Techniques for Efficient Formal Verification Using Binary Decision Diagrams”. PhD thesis, Stanford University. Internet: http://i.stanford.edu/pub/cstr/reports/cs/tr/95/1561/CS-TR-95-1561.pdf, 1995 [Mar. 29, 2016].
  • B. Bingham, J. Bingham, F. M. De Paula, J. Erickson, G. Singh, M. Reitblatt. “Industrial Strength Distributed Explicit State Model Checking”, in Proceedings of the 2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology (PDMC-HIBI ’10). IEEE Computer Society, Washington, DC, USA, 2010, pp. 28-36.
  • W. Jamroga, N. Bulling. “Comparing variants of strategic ability”, in Proceedings of the Twenty-Second international joint conference on Artificial Intelligence – Volume One, 2011, pp. 252-257.
  • F. L. Stoica, M. F. Boian. “Algebraic approach to implementing an ATL model checker”. Studia Univ. Babes Bolyai, Informatica, Cluj-Napoca, Romania. Volume LVII, Number 2, pp. 73–82, 2012.
  • T. Parr. The Definitive ANTLR Reference. Pragmatic Bookshelf, Dallas Texas, ISBN 0-9787392-5-6, 2007.
  • W. Jamroga. “Easy Yet Hard: Model Checking Strategies of Agents”. Computational Logic in Multi-Agent Systems. Lecture Notes in Computer Science, Volume 5405, Springer Berlin Heidelberg, pp. 1-12, 2009.
  • M. Herschel. “Introduction to Database Management Systems”. Internet: https://www.lri.fr/~herschel/courses_ws1314/resources/05_relational_algebra.pdf , 2013 [Mar. 29, 2016].

CITATIONS

Citations used in the publication “Scalability in Model Checking through Relational Databases”.

Currently there are no citations collected for this publication at scholarlyabstracts.com.

-

CONTACT US

Please feel free to us at scholarlyabstracts@gmail.com if you wish to:

  • Get your journal, conference or thesis, registered with us.
  • Update this publication content.

Related Posts

Scroll to Top