Approach for the Formal Specification, Modelling, and Verification of a Safety-critical Multi-agent System; An Employees Management Multi-agent System (EM-MAS)

Abstract

In today’s advanced software technology, intelligent agents are getting more popular. Agent-based technology offers a new dimension for designing and implementing intelligent software systems. Intelligent agents are autonomous and they can make decisions with very little or sometimes no supervision. A multi-agent system comprises multiple intelligent agents that exhibit intelligent and autonomous behavior. In addition, intelligent agents work with minimum or no direct human interaction and have control of their actions as well as their internal states. The goal of employees management multi-agent system is to provide principles and mechanisms for constructing a fault-tolerant distributed system. The multiple autonomous software agents can be used for managing the communication, cooperation, and coordination between these autonomous agents and their continuously changing environment. Autonomous distributed multi-agents are used in employee management systems, for the flexible, adaptable and fault-tolerant environment. The distributed nature of this system, make it fault-tolerant and error-free as it keeps on working if some agents go fail. The Employees Management Multi-Agent System (EM-MAS) is designed, modeled and verified using a formal approach. This formal approach is based on mathematical concepts of Regular expression, First-order predicate calculus, functions, relations, and set theory. Gaia multi-agent methodology is being used for specification, analysis, preliminary design and detailed design of the system. It is centered on the idea of a system as a computational organization consisting of interacting agents with each agent having one or more roles. We have specified, analyzed and proposed a preliminary and detailed design based on Gaia methodology. The system is formally modeled and verified by constructing the system in the form of Coloured Petri Nets (CP-Nets). Formal verification ensures the correctness properties of the proposed model.