Home   >   CSC-OpenAccess Library   >    Manuscript Information
Full Text Available

(600.62KB)
This is an Open Access publication published under CSC-OpenAccess Policy.
Scalability in Model Checking through Relational Databases
Florin Stoica
Pages - 1 - 22     |    Revised - 30-04-2016     |    Published - 01-06-2016
Volume - 4   Issue - 1    |    Publication Date - June 2016  Table of Contents
MORE INFORMATION
KEYWORDS
ATL, Model Checking, Web Services, Relational Algebra, SQL.
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 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.
CITED BY (0)  
1 Google Scholar
2 CiteSeerX
3 Scribd
4 SlideShare
5 PdfSR
1 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.
2 F. L. Cacovean. “Using CTL Model Checker for Verification of Domain Application Systems”, in Proceedings of the 11th International Conference on EVOLUTIONARY COMPUTING (EC '10), 13-15 Jun., Iasi, Romania, ISSN: 1790-2769, ISBN: 978-960-474-194-6, 2010, pp. 262-267.
3 R. Alur, T. A. Henzinger, O. Kupferman. “Alternating-time Temporal Logic”. Journal of the ACM, vol. 49, pp. 672–713, 2002.
4 M. Kacprzak, W. Penczek. “Fully symbolic Unbounded Model Checking for Alternating-time Temporal Logic”. Journal Autonomous Agents and Multi-Agent System, Volume 11 Issue 1, pp. 69 – 89, 2005.
5 R.E. Bryant. “Graph-based algorithms for boolean function manipulation”. IEEE Transactions on Computers, C-35(8), pp. 677-691, 1986.
6 K.Y. Rozier. “Survey: Linear Temporal Logic Symbolic Model Checking”. Computer Science Review, Volume 5 Issue 2, pp. 163-203, 2011.
7 R. Alur, T.A. Henzinger, F.Y.C. Mang, S. Qadeer, S.K. Rajamani, S. Tasiran. “Mocha: Modularity in Model Checking”, in Proceedings of the Tenth International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 1427, Springer, 1998, pp. 521-525.
8 Lomuscio, F. Raimondi. “MCMAS: A model checker for multi-agent systems”, in Proceedings of TACAS 06, volume 3920 of Lect. Notes in Computer Science, Springer-Verlag, 2006, pp. 450-454.
9 C. Eisner, D. Peled. “Comparing Symbolic and Explicit Model Checking of a Software System”, in Proceedings SPIN Workshop on Model Checking of Software, volume 2318 of LNCS, Volume 55, pp. 230-239, 2002.
10 G. Holzmann. “The model checker SPIN”. IEEE Trans. on Software Engineering, vol. 23, pp. 279–295, 1997.
11 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.
12 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].
13 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.
14 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.
15 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.
16 T. Parr. The Definitive ANTLR Reference. Pragmatic Bookshelf, Dallas Texas, ISBN 0-9787392-5-6, 2007.
17 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.
18 M. Herschel. “Introduction to Database Management Systems”. Internet: https://www.lri.fr/~herschel/courses_ws1314/resources/05_relational_algebra.pdf , 2013 [Mar. 29, 2016].
19 T. Rus, E.V. Wyk, T. Halverson. “Generating Model Checkers from Algebraic Specifications”. Journal Formal Methods in System Design archive, Volume 20, Issue 3, pp. 249 – 284, 2002.
20 J. Ebert. “A Versatile Data Structure for Edge-Oriented Graph Algorithms”. Communications of the ACM, Volume 30 Number 6, pp. 513-519, 1987.
21 M. Pistore, P. Traverso. “Planning as model checking for extended goals in non- deterministic domains”, in Proceedings of IJCAI, 2001, pp. 479-486.
22 H2 Database Engine, Internet: http://www.h2database.com/html/performance.html, 2014 [Mar. 29, 2016].
23 D. Owen, T. Menzies. “Lurch: a Lightweight Alternative to Model Checking”, in Proc. Software Engineering and Knowledge Engineering (SEKE), 2003, pp. 158-165.
24 J. Ruan. “Reasoning about Time, Action and Knowledge in Multi-Agent Systems”. Ph.D. Thesis, University of Liverpool. Internet: http://ac.jiruan.net/thesis/, 2008 [Mar. 29, 2016].
25 F. L. Cacovean. “An Algebraic Specification for CTL with Time Constraints”, in Proc. First International Conference on Modelling and Development of Intelligent Systems, Oct. 22-25, Sibiu, Romania, ISSN 2067 – 3965, 2009, pp. 46-55.
Dr. Florin Stoica
Department of Mathematics and Computer Science, Lucian Blaga, University of Sibiu - Romania
florin.stoica@ulbsibiu.ro