Verification of JADE Agents Using ATL Model Checking
Keywords:
Model checking, ATL, agents, JADE, FSMAbstract
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.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.
Published
Issue
Section
License
ONLINE OPEN ACCES: Acces to full text of each article and each issue are allowed for free in respect of Attribution-NonCommercial 4.0 International (CC BY-NC 4.0.
You are free to:
-Share: copy and redistribute the material in any medium or format;
-Adapt: remix, transform, and build upon the material.
The licensor cannot revoke these freedoms as long as you follow the license terms.
DISCLAIMER: The author(s) of each article appearing in International Journal of Computers Communications & Control is/are solely responsible for the content thereof; the publication of an article shall not constitute or be deemed to constitute any representation by the Editors or Agora University Press that the data presented therein are original, correct or sufficient to support the conclusions reached or that the experiment design or methodology is adequate.
