Verification of JADE Agents Using ATL Model Checking

  • Laura Florentina Stoica Faculty of Science, "Lucian Blaga" University of Sibiu
  • Florin Stoica Faculty of Science, "Lucian Blaga" University of Sibiu
  • Florian Mircea Boian Faculty of Mathematics and Computer Science, “Babes-Bolyai” University of Cluj-Napoca,

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.

Author Biographies

Laura Florentina Stoica, Faculty of Science, "Lucian Blaga" University of Sibiu
Department of Mathematics and Informatics,Assistant PhD Candidate
Florin Stoica, Faculty of Science, "Lucian Blaga" University of Sibiu
Department of Mathematics and Informatics,Lecturer PhD
Florian Mircea Boian, Faculty of Mathematics and Computer Science, “Babes-Bolyai” University of Cluj-Napoca,
Department of Computer ScienceProfessor PhD

References

[1] 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

[2] 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

[3] 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

[4] 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.

[5] 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

[6] 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

[7] 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.

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

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

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

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

[12] 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

[13] 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.

[14] 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

[15] 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.

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

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

[18] D. Owen, T. Menzies (2003); Lurch: a Lightweight Alternative to Model Checking, In Software Engineering and Knowledge Engineering (SEKE): 158-165.
Published
2015-07-24
How to Cite
STOICA, Laura Florentina; STOICA, Florin; BOIAN, Florian Mircea. Verification of JADE Agents Using ATL Model Checking. INTERNATIONAL JOURNAL OF COMPUTERS COMMUNICATIONS & CONTROL, [S.l.], v. 10, n. 5, p. 718-731, july 2015. ISSN 1841-9844. Available at: <http://univagora.ro/jour/index.php/ijccc/article/view/803>. Date accessed: 23 jan. 2021. doi: https://doi.org/10.15837/ijccc.2015.5.803.

Keywords

Model checking, ATL, agents, JADE, FSM