Model Checking of Multi Agent System Architectures Using BigMC
Formal methods offer a great potential for early integration of verification in the design process. These are based on theories and mathematical notations that allow the formal specification of a program and check its implementation. They offer a global vision and a high-level structure and system organization. In addition, the software architecture plays a key role as a pivot point between the requirements of a system and its implementation. In this paper, we present a formal approach based on Bigraphical Reactive Systems for specifying and verifying the main features of the Multi Agent Systems (MAS) architectures based on the Belief-Desire-Intention (BDI) agent model. The proposed approach supports both the static and dynamic aspects of BDI-MAS architectures at different levels of abstraction. Further, we use automatic proof tool BigMc to analyze the specifications and verify system properties(original abstract)
- Commoncriteriaportal.org, 'Common Criteria : New CC Portal', 2015. [Online]. Available: http://www.commoncriteriaportal.org/. [Accessed: 16- Feb- 2015].
- A. Dib and Z. Sahnoun, 'Formal Specification of Multi-Agent System Architecture', in International Conference on Advanced Aspects of Software Engineering, Constantine, 2014, pp. 65-72.
- R. Milner, 'Bigraphs and Their Algebra', Electronic Notes in Theoretical Computer Science, vol. 209, pp. 5-19, 2008.
- A. Rao and M. Georgeff, 'Modeling rational agents within a BDIarchitecture', Australian Artificial Intelligence Institute, Victoria, Australia, 1991.
- R. MILNER, 'Axioms for bigraphical structure', Math. Struct. in Comp. Science, vol. 15, no. 06, p. 1005, 2005.
- S. Merz, 'Model Checking: A Tutorial Overview', in Modeling and Verification of Parallel Processes, 2001, pp. 3-38.
- S. Merz, 'Model Checking Techniqes for the Analysis of Reactive Systems', Synthese, vol. 133, no. 12, pp. 173-201, 2002
- G. Perrone, S. Debois and T. Hildebrandt, 'A model checker for Bigraphs', Proceedings of the 27th Annual ACM Symposium on Applied Computing - SAC '12, 2012.
- R. Allen, 'A Formal Approach to Software Architecture', Phd, Carnegie Mellon University, 1997.
- I. Malavolta, P. Lago, H. Muccini, P. Pelliccione and A. Tang, 'What Industry Needs from Architectural Languages: A Survey', IIEEE Trans. Software Eng., vol. 39, no. 6, pp. 869-891, 2013.
- N. Medvidovic and R. Taylor, 'A classification and comparison framework for software architecture description languages', IIEEE Trans. Software Eng., vol. 26, no. 1, pp. 70-93, 2000.
- R. Allen, R. Douence and D. Garlan, 'Specifying and analyzing dynamic software architectures', Fundamental Approaches to Software Engineering, pp. 21-37, 1998.
- F. Oquendo, pi-ADL', SIGSOFT Softw. Eng. Notes, vol. 29, no. 3, p. 1, 2004.
- P. Zhang, H. Muccini and B. Li, 'A classification and comparison of model checking software architecture techniques', Journal of Systems and Software, vol. 83, no. 5, pp. 723-744, 2010.
- R. Bordini, M. Fisher, W. Visser and M. Wooldridge, 'Verifying Multi-agent Programs by Model Checking', Autonomous Agents and Multi-Agent Systems, vol. 12, no. 2, pp. 239-256, 2006.
- R. Bordini, M. Fisher, C. Pardavila, W. Visser and M. Wooldridge, 'Model Checking Multi-Agent Programs with CASP', Computer Aided Verification, pp. 110-113, 2003.
- W. Wan, J. Bentahar and A. Ben Hamza, 'Modeling and Verifying Agent-Based Communities of Web Services', Trends in Applied Intelligent Systems, pp. 418-427, 2010.
- D'Inverno, M., Luck, M., Georgeff, M., Kinny, D. and Wooldridge, M. (2004). The dMARS Architecture: A Specification of the Distributed Multi-Agent Reasoning System. Autonomous Agents and Multi-Agent Systems, 9(1/2), pp.5-53.
- Luck, M. and d'Inverno, M. (2006). Formal Methods and Agent- Based Systems. NASA Monographs in Systems and Software Engineering, pp.65-96.
- M. Fisher and M. Wooldridge, 'On the Formal Specification and Verification of Multi-Agent Systems', International Journal of Cooperative Information Systems, vol. 06, no. 01, pp. 37-65, 1997.