Automated analysis of consensus protocol in specifcation of multi-agents coordination
Main Article Content
Abstract
Abstract. Formal specification and reasoning techniques in software modelling are needed to ensure the correctness of the system at the design phase. Event-B is a formal method with support tools that allows the specifcation and verifcation of reactive systems. In this article, we propose an approach to specify capabilities of a number of software agents. We also verify whether these capabilities help the agents to accomplish a task using a support tool of Event-B. In our previous paper, we have presented about the specifcation and verifcation of sequential protocols. We extend in this article the one of combination between the sequential and parallel protocols of multi-agents software.
References
[1] R Carli et al. “Communication constraints in coordinated consensus problems”. In: American Control Conference. IEEE, 2006.
[2] Gerhard Weiss. Multiagent Systems: A Modern Approach to Distributed Artifcial Intelligence. The MIT Press, 2000.
[3] Michael Wooldridge. An Introduction to MultiAgent Systems. John Wiley & Sons, 2002.
[4] J.R. Abrial. The B-Book, Assigning Programs to Meanings. Cambridge University Press,1996.
[5] http://event-b.org.
[6] Ninh-Thuan Truong, Thanh-Binh Trinh, and Viet-Ha Nguyen. “Coordinated consensus analysis of Multi agent systems using Event-B”. In: SEFM'09: Proceedings of the Formal Methods and Software Engineering. IEEE Computer Society, 2009, pp. 201–209.
[7] V. Hilaire et al. “Formal specification approach of role dynamics in agent organisations: Application to the Satisfaction-Altruism Model”. In: Int. Jour. of Software Engineering and Knowledge Engineering 17.5 (2007), pp. 615–641.
[8] Michael Poppleton. “The Composition of Event-B Models”. In: ABZ '08: Proceedings of the 1st international conference on Abstract State Machines, B and Z. London, UK: Springer-Verlag, 2008, pp. 209–222.
[9] Michael Butler. “Decomposition Structures for Event-B”. In: IFM'09: Proceedings of the 7th International Conference on Integrated Formal Methods. Berlin, Heidelberg: Springer-Verlag, 2009, pp. 20–38.
[10] T. Binh Trinh. “Verifying Java concurrent components”. Phd Thesis. Vietnam National University, Hanoi, 2011.
[11] A. Regayeg, A.H. Kacem, and M. Jmaiel. “Specification and verification of multi-agent applications using temporal Z”. In: Intelligent Agent Technology Conference. IEEE Computer Society, 2004, pp. 260–266.
[12] H. Fadil and J. Koning. “A formal approach to model multiagent interactions using the B formal method”. In: International Symposium on Advanced Distributed Systems. Vol. 3563. LNCS. Springer Verlag, 2005, pp. 516–528.
[13] E. Ball and M. Butler. “Event-B patterns for specifying fault-tolerance in Multi-Agent interaction”. In: Proceedings of Methods, Models and Tools for Fault Tolerance. Vol. 5454. LNCS. Springer, 2009.
[14] Arnaud Lanoix. “Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles”. In: TASE '08: Proceedings of the 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering. IEEE Computer Society, 2008.
[15] Sezai Emre Tuna and Rodolphe Sepulchre. “Quantitative convergence analysis of multiagent systems”. In: 7th IFAC Symposium on Nonlinear Control Systems, 2007.
[16] R. Olfati-Saber, J. A. Fax, and R. M. Murray. “Consensus and Cooperation in Networked Multi-Agent Systems”. In: Proceedings of the IEEE, 2007, pp. 215–233.
[2] Gerhard Weiss. Multiagent Systems: A Modern Approach to Distributed Artifcial Intelligence. The MIT Press, 2000.
[3] Michael Wooldridge. An Introduction to MultiAgent Systems. John Wiley & Sons, 2002.
[4] J.R. Abrial. The B-Book, Assigning Programs to Meanings. Cambridge University Press,1996.
[5] http://event-b.org.
[6] Ninh-Thuan Truong, Thanh-Binh Trinh, and Viet-Ha Nguyen. “Coordinated consensus analysis of Multi agent systems using Event-B”. In: SEFM'09: Proceedings of the Formal Methods and Software Engineering. IEEE Computer Society, 2009, pp. 201–209.
[7] V. Hilaire et al. “Formal specification approach of role dynamics in agent organisations: Application to the Satisfaction-Altruism Model”. In: Int. Jour. of Software Engineering and Knowledge Engineering 17.5 (2007), pp. 615–641.
[8] Michael Poppleton. “The Composition of Event-B Models”. In: ABZ '08: Proceedings of the 1st international conference on Abstract State Machines, B and Z. London, UK: Springer-Verlag, 2008, pp. 209–222.
[9] Michael Butler. “Decomposition Structures for Event-B”. In: IFM'09: Proceedings of the 7th International Conference on Integrated Formal Methods. Berlin, Heidelberg: Springer-Verlag, 2009, pp. 20–38.
[10] T. Binh Trinh. “Verifying Java concurrent components”. Phd Thesis. Vietnam National University, Hanoi, 2011.
[11] A. Regayeg, A.H. Kacem, and M. Jmaiel. “Specification and verification of multi-agent applications using temporal Z”. In: Intelligent Agent Technology Conference. IEEE Computer Society, 2004, pp. 260–266.
[12] H. Fadil and J. Koning. “A formal approach to model multiagent interactions using the B formal method”. In: International Symposium on Advanced Distributed Systems. Vol. 3563. LNCS. Springer Verlag, 2005, pp. 516–528.
[13] E. Ball and M. Butler. “Event-B patterns for specifying fault-tolerance in Multi-Agent interaction”. In: Proceedings of Methods, Models and Tools for Fault Tolerance. Vol. 5454. LNCS. Springer, 2009.
[14] Arnaud Lanoix. “Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles”. In: TASE '08: Proceedings of the 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering. IEEE Computer Society, 2008.
[15] Sezai Emre Tuna and Rodolphe Sepulchre. “Quantitative convergence analysis of multiagent systems”. In: 7th IFAC Symposium on Nonlinear Control Systems, 2007.
[16] R. Olfati-Saber, J. A. Fax, and R. M. Murray. “Consensus and Cooperation in Networked Multi-Agent Systems”. In: Proceedings of the IEEE, 2007, pp. 215–233.