Verification of JADE Agents Using ATL Model Checking

Laura Florentina Stoica, Florin Stoica, Florian Mircea Boian

Abstract


It is widely accepted that the key to successfully developing a system is to produce a thorough system specification and design. This task requires an appropriate formal method and a suitable tool to determine whether or not an implementation conforms to the specifications. In this paper we present an advanced technique to analyse, design and debug JADE software agents, using Alternating-time Temporal Logic (ATL) which is interpreted over concurrent game structures, considered as natural models for compositions of open systems. In development of the proposed solution, we will use our original ATL model checker. In contrast to previous approaches, our tool permits an interactive or programmatic 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.

Keywords


Model checking, ATL, agents, JADE, FSM

Full Text:

PDF

References


K.Y. Rozier (2011); Survey: Linear Temporal Logic Symbolic Model Checking, Computer Science Review, vol. 5, Issue 2: 163-203.
http://dx.doi.org/10.1016/j.cosrev.2010.06.002

J. Barnat, L. Brim, P. Rockai (2010); Scalable Shared Memory LTL Model Checking, International Journal on Software Tools for Technology Transfer (STTT), 12(2): 139-153.
http://dx.doi.org/10.1007/s10009-010-0136-z

R. Alur, T.A. Henzinger, O. Kupferman (2002); Alternating-time temporal logic, Journal of the ACM, 49(5): 672-713.
http://dx.doi.org/10.1145/585265.585270

M. Kacprzak, W.Penczek (2005); Fully symbolic Unbounded Model Checking for Alternating-time Temporal Logic, Journal Autonomous Agents and Multi-Agent System, 11(1): 69-89.

R. Alur et al (1998); Mocha: modularity in model checking, in Proc. Of CAV 98, vol. 1427 of Lect. Notes in Comp. Sci., Springer-Verlag: 521-525.
http://dx.doi.org/10.1007/bfb0028774

A. Lomuscio, F.Raimondi (2006); Mcmas: A model checker for multi-agent systems, in Proc. of TACAS 06, vol. 3920 of Lect. Notes in Comp. Sci., Springer-Verlag: 450-454.
http://dx.doi.org/10.1007/11691372_31

F. Stoica, L.F. Cacovean (2014); Implementing an ATL Model Checker tool using Relational Algebra concepts, in Proceeding The 22th International Conference on Software, Telecommunications and Computer Networks (SoftCOM): 361-366.

W. Van der Hoek, M. Wooldridge (2002); Tractable multiagent planning for epistemic goals, in Proceedings of AAMAS-02, ACM Press: 1167-1174.

L.F. Stoica, F. Stoica ; WebCheck - ATL/CTL model checker tool, http://use-it.ro

Java Agent Development Framework (JADE), http://jade.tilab.com/

F. Bellifemine, G. Caire, T. Trucco, G. Rimassa (2013); JADE programmer's guide, http://jade.tilab.com

R. E. Bryant (1986); Graph-based algorithms for boolean function manipulation, IEEE Transactions on Computers, C-35(8): 677-691.
http://dx.doi.org/10.1109/TC.1986.1676819

C. Eisner, D. Peled (2002); Comparing Symbolic and Explicit Model Checking of a Software System, In Proc. SPIN Workshop on Model Checking of Software, volume 2318 of LNCS, Volume 55: 230-239.

F. Lerda, N. Sinha, M. Theobald (2003); Symbolic Model Checking of Software, Electronic Notes in Theoretical Computer Science, 89(3): 480-498.
http://dx.doi.org/10.1016/S1571-0661(05)80008-8

B. Bingham, J. Bingham, F. M. de Paula,; J. Erickson, G. Singh, M. Reitblatt (2010); Industrial Strength Distributed Explicit State Model Checking, Proc.of the 2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second Int. Workshop on High Performance Computational Systems Biology (PDMC-HIBI '10), IEEE Computer Society, Washington, DC, USA, 28-36.

A. J. Hu (1995); Techniques for Efficient Formal Verification Using Binary Decision Diagrams, PhD thesis, Stanford University.

J. Ruan (2008); Reasoning about Time, Action and Knowledge in Multi-Agent Systems, Ph.D. Thesis, University of Liverpool, http://ac.jiruan.net/thesis/.

D. Owen, T. Menzies (2003); Lurch: a Lightweight Alternative to Model Checking, In Software Engineering and Knowledge Engineering (SEKE): 158-165.




DOI: https://doi.org/10.15837/ijccc.2015.5.803



Copyright (c) 2017 Laura Florentina Stoica, Florin Stoica, Florian Mircea Boian

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.

IJCCC is an Open Access Journal : CC-BY-NC.

Articles published in IJCCC user license are protected by copyright.

Users can access, download, copy, translate the IJCCC articles for non-commercial purposes provided that users, but cannot redistribute, display or adapt:

  • Cite the article using an appropriate bibliographic citation: author(s), article title, journal, volume, issue, page numbers, year of publication, DOI, and the link to the definitive published version on IJCCC website;
  • Maintain the integrity of the IJCCC article;
  • Retain the copyright notices and links to these terms and conditions so it is clear to other users what can and what cannot be done with the  article;
  • Ensure that, for any content in the IJCCC article that is identified as belonging to a third party, any re-use complies with the copyright policies of that third party;
  • Any translations must prominently display the statement: "This is an unofficial translation of an article that appeared in IJCCC. Agora University  has not endorsed this translation."

This is a non commercial license where the use of published articles for commercial purposes is forbiden. 

Commercial purposes include: 

  • Copying or downloading IJCCC articles, or linking to such postings, for further redistribution, sale or licensing, for a fee;
  • Copying, downloading or posting by a site or service that incorporates advertising with such content;
  • The inclusion or incorporation of article content in other works or services (other than normal quotations with an appropriate citation) that is then available for sale or licensing, for a fee;
  • Use of IJCCC articles or article content (other than normal quotations with appropriate citation) by for-profit organizations for promotional purposes, whether for a fee or otherwise;
  • Use for the purposes of monetary reward by means of sale, resale, license, loan, transfer or other form of commercial exploitation;

    The licensor cannot revoke these freedoms as long as you follow the license terms.

[End of CC-BY-NC  License for Website User]


INTERNATIONAL JOURNAL OF COMPUTERS COMMUNICATIONS & CONTROL (IJCCC), With Emphasis on the Integration of Three Technologies (C & C & C),  ISSN 1841-9836.

IJCCC was founded in 2006,  at Agora University, by  Ioan DZITAC (Editor-in-Chief),  Florin Gheorghe FILIP (Editor-in-Chief), and  Misu-Jan MANOLESCU (Managing Editor).

Ethics: This journal is a member of, and subscribes to the principles of, the Committee on Publication Ethics (COPE).

Ioan  DZITAC (Editor-in-Chief) at COPE European Seminar, Bruxelles, 2015:

IJCCC is covered/indexed/abstracted in Science Citation Index Expanded (since vol.1(S),  2006); JCR2018: IF=1.585..

IJCCC is indexed in Scopus from 2008 (CiteScore2018 = 1.56):

Nomination by Elsevier for Journal Excellence Award Romania 2015 (SNIP2014 = 1.029): Elsevier/ Scopus

IJCCC was nominated by Elsevier for Journal Excellence Award - "Scopus Awards Romania 2015" (SNIP2014 = 1.029).

IJCCC is in Top 3 of 157 Romanian journals indexed by Scopus (in all fields) and No.1 in Computer Science field by Elsevier/ Scopus.

 

 Impact Factor in JCR2018 (Clarivate Analytics/SCI Expanded/ISI Web of Science): IF=1.585 (Q3). Scopus: CiteScore2018=1.56 (Q2);

SCImago Journal & Country Rank

Editors-in-Chief: Ioan DZITAC & Florin Gheorghe FILIP.