CFP last date
20 May 2024
Reseach Article

Rewriting Logic based Approach for the Formalization of Critical Systems based on Multi-Agent System

by Ammar Boucherit, Abdallah Khebaba, Faiza Belala
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 13 - Number 2
Year of Publication: 2011
Authors: Ammar Boucherit, Abdallah Khebaba, Faiza Belala
10.5120/1755-2392

Ammar Boucherit, Abdallah Khebaba, Faiza Belala . Rewriting Logic based Approach for the Formalization of Critical Systems based on Multi-Agent System. International Journal of Computer Applications. 13, 2 ( January 2011), 6-13. DOI=10.5120/1755-2392

@article{ 10.5120/1755-2392,
author = { Ammar Boucherit, Abdallah Khebaba, Faiza Belala },
title = { Rewriting Logic based Approach for the Formalization of Critical Systems based on Multi-Agent System },
journal = { International Journal of Computer Applications },
issue_date = { January 2011 },
volume = { 13 },
number = { 2 },
month = { January },
year = { 2011 },
issn = { 0975-8887 },
pages = { 6-13 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume13/number2/1755-2392/ },
doi = { 10.5120/1755-2392 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T20:01:41.276472+05:30
%A Ammar Boucherit
%A Abdallah Khebaba
%A Faiza Belala
%T Rewriting Logic based Approach for the Formalization of Critical Systems based on Multi-Agent System
%J International Journal of Computer Applications
%@ 0975-8887
%V 13
%N 2
%P 6-13
%D 2011
%I Foundation of Computer Science (FCS), NY, USA
Abstract

The agent-oriented paradigm is an emerging technology, which has significant and growing interest, particularly through its ability to be used in the modeling of all types of systems and representation of knowledge. However, this potentiality should not hide the difficulties associated with them in the design and verification, which may cause the scientific credibility of multi-agent modeling field, especially for the case of embedded and critical systems.

References
  1. F. Belala, A. Boucherit. Contribution to the Formal Checking of Multi-Agents Systems. Proceedings of the IEEE International Conference on Computer Systems and Applications, ISBN: 1-4244-0211-5, 2006, pp. 9-16.
  2. F. Belala, A. Boucherit. Towards a Videoconference Interface Formalisation, The 4th International Arab Conference on computer science and Information Technology, CSIT06, 2006.
  3. C. Lobry, H. Elmoznino. Combinatorial Properties of Some Cellular Automata Related to the Mosaic Cycle Concept, Acta Biotheoretica, Volume 48, Issue 3 - 4, Dec 2000, pp 219 - 242.
  4. A. Pavé. Modélisation en biologie et en écologie. ALEAS Ed, Lyon, 1994, 560 p.
  5. M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st IEEE Symp. Logic in Computer Science (LICS'86), Cambridge, MA, USA, June 1986, pp 332–344.
  6. O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the 12th ACM Symp. Principles of Programming Languages (POPL'85), New Orleans, LA, USA, 1985, pp 97–107.
  7. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. In ACM Transactions on Programming Languages and Systems, volume 8, April 1986, pp 244–263.
  8. N. Marti-Oliet, J. Meseguer, Rewriting Logic as a Logical and Semantic Framework, Electronic Notes in Theoretical Computer Science, Vol 4, no1, 1996, pp1-36.
  9. N. Marti-Oliet, J. Meseguer, Rewriting Logic as a Logical and Semantic Framework, Technical Report SRI-CSL-93-05, Menlo Park, CA 94025, and Center for the study of language and Information Stanford University, Stanford, CA 94305, 1993.
  10. J. Meseguer. Conditional rewriting logic as a unified model of concurrency, technical report SRI CSL 91. 1991.
  11. J. Meseguer. Rewriting Logic Revisited, Slides of tutorial presented at WRLA 2002, Pisa, Italy, September 2002.
  12. M.O. Stehr, José Meseguer, and Peter C. Ölveczky. Rewriting Logic as a Unifying Framework for Petri Nets. In Unifying Petri Nets. Lecture Notes in Computer Science (Advances in Petri Nets). 2001.
  13. J. Meseguer, Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 1992, pp 73–155.
  14. A. Verdejo and N. Mart-Oliet. Executing E-LOTOS processes in MAUDE. In H. Ehrig, M. Grosse-Rhode, and F. Orejas, editors, INT 2000, Integration of Specification Techniques with Applications in Engineering, Extended Abstracts, pp 49-53. Technical report 2000/04, Technische Universitat Berlin, March 2000.
  15. A. Verdejo and N. Mart -Oliet. Implementing CCS in MAUDE. In T. Bolognesi and D. Latella, editors, Formal Methods For Distributed System Development. FORTE/PSTV 2000 IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX) October 2000, Pisa, Italy, Kluwer Academic Publishers, 2000, pp 351-366.
  16. V. López, J. Alberto, N.Martí Oliet, Executing and verifying CCS in MAUDE. Technical report, 99-00. pp 1-47.
  17. M.O. Stehr and C. Talcott. PLAN in MAUDE: Specifying an active network programming language. In F. Gadducci and U. Montanari, editors, Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, 2002.
  18. P.Thati, S. Koushik, N. Marti-Oliet. An Executable Specification of Asynchronous Pi-Calculus Semantics and May Testing in MAUDE 2.0. In 4th International Workshop on Rewriting Logic and its Applications (WRLA'02).
  19. Projet SPECTRE : Spécification et programmation des systèmes communicants et temps réel. Rapport d’activité INRIA 1996.
  20. A. Benzakour. Vérification formelle des systèmes parallèles, Mémoire présenté à la Faculté des études supérieures de l'université Laval pour l'obtention du grade de Maître ès Sciences. 1997.
  21. P. R. Cohen and H. J. Levesque. Intention is choice with commitment. Artificial Intelligence, AI, 42(2-3):213-261, March 1990.
  22. M. Wooldridge. Temporal belief logics for modeling artificial intelligence systems. Foundations of distributed artificial intelligence. Wiley-Interscience, 1996.
  23. A. Haddadi. Communication and Cooperation in Agent Systems. Lecture Notes in Artificial Intelligence, 1996.
  24. M. Benerecetti, F. Giunchiglia, and L. Serafini. Model checking multiagent systems. Journal of Logic and Computation, 8(3):401 423, June 1998.
  25. M.Wooldridge. Reasoning about Rational Agents. Intelligent Robots and Autonomous Agents. The MIT Press, Cambridge, Massachusetts, 2000.
  26. D. Moldt and F. Wienberg, Multi-agent systems based on coloured Petri nets, in Application and Theory of Petri Nets 1997, eds. P. Azema and G. Balbo (Springer, Berlin, 1997) pp. 82-101.
  27. A. Lomuscio and M. Sergot. The bit transmission problem revisited. Technical Report 4/2002, department of computing, Imperial College, London SW7 2BZ, UK, 2002.
  28. W. van der Hoek and M. Wooldridge. Towards a logic of rational agency. Logic Journal of the IGPL, 11(2):133-157, March 2003.
  29. P. Bommel. Définition d’un cadre méthodologique pour la conception de modèles multi-agents adaptée à la gestion des ressources renouvelables. Thèse de doctorat en informatique de l’université de Montpellier II-Sciences et Techniques du Languedoc. 2009.
  30. Ramat, E. Introduction à la modélisation et à la simulation à événements discrets. In : Modélisation et simulation multi-agents pour les Sciences de l'Homme et de la Société, Amblard F. and Phan D. (eds.), Londres, Hermes-Sciences & Lavoisier, ISBN : 2-7462-1310-9. 2006.
  31. G. Quesnel. Approche formelle et opérationnelle de la multi-modélisation et de la simulation des systèmes complexes. Thèse de doctorat en informatique à l’école doctorale de l’université du Littoral - Côte d’Opale. 2006.
  32. H. ZWIRN Les limites de la connaissance, Paris, Odile Jacob, 2000.
  33. K. Havelund, A. Skou, G. Larsen, K. Lund. Formal modeling and analysis of an audio/video protocol : An industrial case study using UPPAAL. In Proc. 18th IEEE Real-Time Systems Symposium (RTSS'97), IEEE Computer Society Press, pp 2–13, 1997.
  34. S. Tripakis, S. Yovine. Verification of the fast reservation protocol with delayed transmission using the tool KRONOS. In Proc. 4th IEEE Real-Time Technology and Applications Symposium (RTAS'98), IEEE Computer Society Press, pp 165–170, 1998.
  35. N. R. Jennings. On Agent Based Software Engineering. Artificial Intelligence. Vol. 117, 2000, p. 277-296.
  36. J..C. Fernandez, C.Jard, T.Jron, C.Viho, Using on-the-fly verification techniques for the generation of test suites, in Proceedings of Conference on Computer-Aided Verification (CAV ’96), LNCS 1102, pp. 348-359, Springer, 1996.
  37. G. Bhat, R. Cleaveland, O. Grumberg, Efficient on-the-fly Model checking for CTL*, in Prooceedongs of Symposium on Logics in Computer Science, pp.388-397, IEEE, 1995.
  38. M. Clavel. Strategies and User Interfaces in Maude at Work. WRS 2003, 3rd International Workshop on Reduction Strategies in Rewriting and Programming - Final Proceedings. Volume 86, Issue 4, December 2003, Pages 570-592.
  39. S. Eker, J. Meseguer, A. Sridharanarayanan. The Maude LTL Model Checker. Electronic Notes in Theoretical Computer Science, Volume 71. From Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications (WRLA 2002). Edited by Fabio Gaducci and Ugo Montanari. Elsevier, Amsterdam. September, 2002.
  40. M. Wooldridge. An Introduction to MultiAgent Systems - Second Edition, Published May 2009 by John Wiley & Sons. ISBN-10: 0470519460.
  41. M. Wooldridge and N. R. Jennings. Intelligent Agents: Theory and Practice. The Knowledge Engineering Review, 10(2), 1995.
  42. D. T. Ndumu and H. S. Nwana. Research and development challenges for agent-based systems. IEE Proc. of Software Engineering, 144(1), 1997.
  43. M. Dastani, K. V. Hindriks, J.C. Meyer. Specification Language and Verification Environment. 1st Edition, 2010, XVII, 405 p. 100 illus., Hardcover. Publisher: Springer. ISBN: 978-1-4419-6983-5.
  44. S. Shapiro, Y. Lespérance, and H.J. Levesque. The cognitive agents specification language and verification environment for multiagent systems, in Proc. AAMAS, 2002, pp.19-26.
  45. B. Bauer, J. P. Muller, J. Odell. Agent UML: A Formalism for Specifying Multiagent Interaction. Agent-Oriented Software Engineering, Paolo Ciancarini and Michael Wooldridge eds., Springer, Berlin, pp. 91-103, 2001.
  46. L. Kahloul, K. Barkaoui, Z. Sahnoun, Using AUML to derive formal modeling agents interactions, aiccsa, pp.109-vii, ACS/IEEE 2005 International Conference on Computer Systems and Applications (AICCSA'05), 2005.
  47. H. Lin, Designing Multi-Agent Systems from Logic Specifications: A Case Study, in Vijay Sugumaran (ed.), Distributed Artificial Intelligence, Agent Technology, and Collaborative Applications, IGI Global, 2008, pp. 1-27.
  48. Duboz R., D. Versmisse, G. Quesnel, A. Muzzy, E. Ramat. Specification of Dynamic Structure Discret event Multiagent Systems 2006 Agent-Directed Simulation (ADS 2006). Huntsville, AL, USA, April 2-6 2005.
  49. H. Xu and S. M. Shatz, “An Agent-Based Petri Net Model with Application to Seller/Buyer Design in Electronic Commerce,” Proceedings of the IEEE 5th International Symposium on Autonomous Decentralized Systems (ISADS), Dallas, Texas, March 2001, pp. 11-18.
  50. V. Mascardi. M. Martelli and L. Sterling. Logic-Based Specification Languages for Intelligent Software Agents. Theory and Practice of Logic Programming Journal (TPLP). Volume 4 Issue 4, July 2004. publisher Cambridge University Press, pp. 429-494.
  51. M. Martelli, V. Mascardi, Floriano Zini. Specification and Simulation of Multi-Agent Systems in CaseLP. APPIA-GULP-PRODE'1999. pp.13-28.
  52. H. Zhu, SLABS: A Formal Specification Language for Agent-Based Systems, International Journal of Software Engineering and Knowledge Engineering, Vol. 11. No. 5, pp529~558.
  53. Finin, T., Labrou, Y.: KQML as an agent communication language. In J.M. Bradshaw (ed.), Software Agents, MIT Press, Cambridge, MA, (1997), 291-316.
  54. A. Lomuscio, M. J. Sergot: On Multi-agent Systems Specification via Deontic Logic. ATAL 2001. International workshop No8, Seattle WA , ETATS-UNIS2002 , vol. 2333, pp. 86-99.
  55. R. Cervenka, I. Trencanský, M. Calisti: Modeling Social Aspects of Multi-Agent Systems: The AML Approach. AOSE 2005. pp. 28-39.
  56. L.S. Sterling, K.Taveter, The Art of Agent-Oriented Modeling. The MIT Press 2009.
  57. D.S. Dillon, T.S. Dillon, and E. Chang, “Using UML 2.1 to model. Multi- Agent Systems”, Proceedings of the 6th IFIP Workshop on. Software Technologies for Future Embedded and Ubiquitous Systems,. Italy, 2008.
  58. I. Trencansky and R. Cervenka, Agent Modeling Language (AML): A comprehensive approach to modeling MAS, Informatica 29(4) 2005 391-400.
  59. Aihua Ren, Hui Jiao, Yunfeng Sun: Modeling Mobile Agent with Object-Oriented Petri Net. ACTA AERONAUTICA ET ASTRONAUTICA SINICA. Vol.24 No.1 (Sum No.182) (2003) 57-61.
  60. H. Lin and C. Yang, C. Spécification de systèmes multi-agent dans le langage Gamma. Proceedings of the IEEE 19th Annual Canadian Conference on Electrical and Computer Engineering (CCECE05). Ottawa, Ontario, Canada. Du 7 au 10 mai 2006. Numéro de publication du CNRC : NRC 48476.
  61. F. Mokhati, M. Badri, L. Badri: A Formal Framework Supporting the Specification of the Interactions between Agents. Informatica (Slovenia) 31(3). Pp. 337-350. 2007.
  62. B. Chen, S. Sadaoui. A Generic Formal Framework for Multi-agent Interaction Protocols. Technical Report TR 2004-05 ISBN 0-7731-0483-6 Department of Computer Science, University of Regina, Regina SK, Canada, 2004.
  63. D. Kinny, M. Georgeff, and A. Rao, “A Methodology and Modeling Technique for Systems of BDI Agents,” Tech. Rep. 58, Australian Artificial Intelligence Institute, Melbourne, Australia, Jan. 1996.
  64. M. Wooldridge, 1996. “A logic for BDI planning agents” In Pierre-Yves Schobbens, editor, Working Notes of 2nd ModelAge Workshop: Formal Models of Agents, Sesimbra, Portugal
  65. M. Fisher, 1996. An introduction to executable temporal logics. Knowledge Engineering Review, 11(1). pp. 43–56.
  66. M. Wooldridge, N. Jennings and D. Kinny, The GAIA Methodology for agent-oriented analysis and design, Autonomous Agents and Multi-Agent Systems 3(3) (2000) 285-312.
  67. A. Mohammed, U. Furbach. Multi-agent Systems:Modeling and verification Using Hybrid Automata. In Lars Braubach, Jean-Pierre Briot, and John Thangarajah, editors, Revised and Invited Papers of the post-proceedings of 7th International Workshop on Programming Multi-Agent Systems (ProMAS2009), LNAI 5919, pages 49-66, Springer.
Index Terms

Computer Science
Information Sciences

Keywords

Critical System Model-Checking Multi-agent systems Maude Rewriting logic Specification Testing Verification