Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2015 | 5 | 1717--1722
Tytuł artykułu

Model Checking of Multi Agent System Architectures Using BigMC

Warianty tytułu
Języki publikacji
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)
Słowa kluczowe
Opis fizyczny
  • University of Constantine II.
  • University of Constantine II
  •, 'Common Criteria : New CC Portal', 2015. [Online]. Available: [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.
Typ dokumentu
Identyfikator YADDA

Zgłoszenie zostało wysłane

Zgłoszenie zostało wysłane

Musisz być zalogowany aby pisać komentarze.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.