Keywords

1 Introduction

The most challenging thing in software engineering for Multi-Agent is to ensure that the requirement of the system is well identified and verified [1, 2], especially when the system is complex and appeals with many stakeholders. In this paper, we are interested to study the Multi-Agent system to cope with the dynamic, distributed and cooperative systems. A multi-agent system is a system made up of several agents which are in interaction among them, this interaction is very important to define the overall behavior of the system. The behavior of the agent is defined to be a set of properties that an agent outlines to give responses to its environment [3]. Basically, the agent reacts to events based on the received decisions and gives responses in the form of actions according to the experienced situation.

To specify MAS, it is important to have processes and methods that will help engineers to understand how to build up customized system [4]. In this paper, we are interested of studying the specification of five essential properties that the agents are supposed to exhibit: reactivity, adaptability, conflict management, and reusability. The reactivity refers to the ability to respond to the environment, the adaptability is the capacity to cope with changes and disruptions of the environment, the conflict management is the ability to manage resource sharing, and the reusability is the capability to reuse agent components. In literature, there are approaches [10,11,12,13,14] that study some of these properties, but there is still a lack of an all-in-one approach that considers all of the mentioned properties.

To deal with the complexity of building up a multi-agent system, this paper proposes a method that helps to make the specification and the verification of such a system to avoid errors happening within the implementation phase. Since MAS can be applied in different domains and systems, this paper proposes to have demonstration of this method through a Crisis Management system case study.

Thus, this paper intends to present the difficulty of how to define the specification of Crisis Management system for both individual and collective behavior. We propose a method called BECAMEDA (Behavioral spEcification and verifiCAtion of RMAS based on E-MDRA) for the specification and the verification of Reactive Multi-Agent System based on the E-MDRA (Extended Multi-Decisional Reactive Agent) model. The E-MDRA is an extension of The MDRA, which is developed by [5], The MDRA is being deployed in various domains such as wireless sensor networks [6], mobile systems [7] and organizational systems [8], this model helps on modeling reactive agents by putting forward decisional aspect facilitating the specification of the agent according to their behavior and their intelligence. Throughout this paper, the Crisis Management system is used as an example to demonstrate our approach [9]. The overall goals of the Crisis Management System (CMS) are: facilitating the rescue mission of the police by offering detailed information about the location of the crash; managing the dispatch of ambulances or other alternate emergency vehicles to transport victims from the crisis scene to hospitals; facilitating the first-aid missions by providing relevant medical history of identified victims to the first-aid workers by querying databases of local hospitals.

The rest of the paper is organized as follows. Section 2 presents a related work. Section 3 presents a background related to the Extended Multi Decisional Reactive Agent. Section 4 describes our approach through an example of a Crisis Management System. Section 5 concludes the paper and draws future perspectives.

2 Related Work

Many approaches have been proposed for the specification and the verification of MAS. [10] presents a formal method for specifying and verifying a Multi-Agent system based on design patterns, refinement, and event-B. The objective of the method is to satisfy the global properties of the system based on the agent’s local behavior. [11] proposes an approach to specify by refinement in event-B the collaboration between agents in a critical system where the consideration of the fault tolerance property is essential. The authors define the SMA through four applets (A, M, E, R). A represents a collection of different classes of agents. Μ represents a middleware system that has the ability to ensure the communication flow between agents and resolve the communication disconnect issues, E represents a collection of system events, R represents a set of dynamic relationships between agents allowing making connections between active agents belonging either to the same classes or to different classes. [12] proposes High Level Multi-Agent Petri-Net (HMAP) to describe, model and analyze the dynamic behavior of MAS based on the Petri Net. HMAP is based on a formal logical method describing the behavior of the agent in nine sequential steps. [13] proposes an approach called ForMAAD (Formal Method for Agent-based Application Design) to specify the agent’s behavior at the individual and the collective levels. The behavior is specified through a formal language called Temporal Z that integrates the first-order temporal logic with the Z notation. The approach proposes to divide the refinement process into four levels: cooperation, organizational, collective behavior and individual behavior. [14] proposes a translation of the AUML (Agent UML) diagrams; which is an extension of the UML language to model Multi-Agent system; into the RT-Maude formal language. RT-Maude supports the specification and the analysis of real-time systems, and more specifically object-oriented real-time systems. It is based on the programming environment based on the rewriting logic.

The Table 1 presents a comparison between the different approaches according to the reactivity, adaptability, conflict management, and reusability properties. We note that there is no specific approach that considers all the properties mentioned. Besides of this, there is a lack of a real process that helps engineer to model the specification phase, which is the most important phase on the software engineer process.

Table 1. Comparison of approaches to specify MAS.
Full size table

In our previous works [15], we have proposed an extension of MDRA model called E-MDRA to deal with the properties mentioned. However, we are still in need to have a method that helps engineers to correctly identify and define the specification. Thus, this paper focuses on the proposed method based on E-MDRA. The next section gives an overview of the E-MDRA specification model.

3 E-MDRA Model Overview

3.1 E-DRA

The E-DRA model is based on an external specification & an internal specification [15]. The external specification denotes a set of information sent to or received from the environment. It is characterized by:

  • A: Set of actions exerted on the agent, each action represents a possible operation to be performed on this agent

  • D: Set of decisions generated by the agent to provide solutions concerning the system behavior. A decision d is characterized by its decision horizon DurDec(d), that indicates the time during which this decision remains valid

  • S: Set of Signal received by the agent. The signal represents the acknowledgement response to confirm the execution of a decision

  • \( \text{E}^{\prime } \): Set of external states delivered by the agent. Each external states represents the object state emitted to the environment

The internal specification represents a set of information generated and exchanged inside the agent. It is characterized by:

  • E: Set of agent’s internal states. Each one indicates the current state of the agent. An agent may exhibits parallel operations

  • O: Set of agent’s internal objectives. Each internal objective denotes the expected state after the execution of a decision

  • \( \text{O}^{{^{\prime } }} \): Set of agent’s external objectives, which can be achieved. These objectives represent the agent interpretation of each action, and define therefore its different behaviors

From a dynamic perspective, these sets determine the events received from the environment (A, S), events sent to the environment (D, E) and the internal events (E, O, \( \text{O}^{\prime } \)).

3.2 E-MDRA

The organization of Extended Multi Decisional Reactive (E-MDRA) is defined by a set of agents connected together with communication interfaces, thus forming a hierarchical structure based on two-level tree: an E-DRA Supervisor (E-DRAS) and two or several sub-agent components (E-MDRASi). The connection between supervisor and its sub-agents is realized through two communication interfaces: Decisional Interface (DI) and Signaling Interface (SI). Such a system interacts with its environment with Actions exerted by the environment and External States emitted to the environment.

The description of a MDRA is defined as a quadruplet S: < E-DRAS, DI, SI, S-MDRA >, with:

  • E-DRAS: represents the E-DRA type that supervises S.

  • DI: Decisional Interface of S, implements a translation function of a decision into several parallel actions, each of these actions belongs to a low-level sub-agent.

  • SI: Signaling Interface of S, implements a translation functions of several external states into one and only signal.

  • S-MDRA: characterizes a set of 2 or more E-MDRA components.

4 BECAMEDA Method

BECAMEDA (Behavioral spEcification and verifiCAtion of RMAS based on E-MDRA) method provides support for the specification and verification of multi-agent with the involvement of the reactivity, the adaptability, the conflicts management and the reusability properties. It captures the requirements and goals of the system, identifies the goal’s actions, determines the system’s organizational structure and models the internal and external behavioral specification of the agents.

BECAMEDA is made up of two layers: specification layer and verification layer. The specification layer is consisted of three phases: identification phase, definition phase and modeling phase. The identification phase is the phase where the system identifies its goals. A goal represents a desirable objective of the system. Goals are organized as a hierarchical structure made up through the refinement of higher-level goals towards lower-level goals. The lower-level goal is achieved through actions. The definition phase consists of two steps: the first step represents the agents and their organizational structure which is also classified into levels. Whereas, the second step determines the actions to be assigned to agents under each level. During this phase, the actions are a priori assigned to agents of level 1, then, according to the modeling phase, they are assigned to the following level. Basically, the modeling phase is made up through three steps for each agent under a level i greater than or equal 1. The First step, models the internal behavior actions of level i. the Second step, assigns actions to agents of the following level (level i + 1), and finally, the third step, models the external behavior actions of level i.

After having establishing the models of the agent for both internal and external behavior, the verification layer indicates the system properties to be verified, and performs afterwards a formal verification with the use of model-checking technique. Figure 1 illustrates the BECAMEDA phases.

Fig. 1.
figure 1

BECAMEDA phases.

Full size image

4.1 Identification Phase

The identification phase captures the system requirements and identifies the goals of the system. A goal defines the global objectives that the system desires to fulfill. This phase is made up following three steps: identifying goals, refining goals and identify goal actions. The two first goals are represented with two models: the goals model and the refined goals model. The goal model facilitates the understanding of a system with the generation of a set of abstract goals that offer a high-level understanding of the defined objective of the system, as for the refined goals model, it identifies the concrete goals that highlight the goal activities. The goal-actions model identifies the actions that realize the concrete goal. The entities forming this phase are built up following the meta-model of Fig. 2 where is defined the concept of goal, action and their different relationships.

Fig. 2.
figure 2

Identification phase metamodel.

Full size image

In the following, we present the BECAMEDA method throughout an example of a Crisis Management system.

Identify goals.

In this step, we represent the system requirements as a set of structured goals consisted of sub-goals. The goals called “abstract goals” express the high-level objective of the system; they are connected by AND/OR/XOR logic gates. The AND indicates that all of the sub-goals must be completed to satisfy the parent goal, the OR indicates that there is an alternative way to represent the sub-goals, and the XOR indicates that the goal parent can be satisfied with one of its sub-goals.

Goal refinement.

We decompose in this step the abstract goal into concrete goals to capture the dynamic aspects of the goals model and defines each goal through “precede” and “trigger” attributes. The “precedes” determines that the goal X must be completed before the goal Y is pursued. Whereas “triggers”, means the instantiation of a new goal when an event occurs while another goal is still in activity.

The Fig. 3 presents the step 1 and 2 of the identification phase. The Goal “capture info Crisis (Goal 1)” depends on the achievement of three concrete goals: “receive information from witnesses (Goal 1.1)”, “receive information from video surveillance (Goal 1.2)” or “receive information from the phone company (Goal 1.3)”. We note that the three sub-goals are successive goals, since they are defined by the key word “preceded” and are alternative as well. Indeed, when a crisis event is reported, the first step to do is to get the maximum information from witnesses, in case of doubt, it is possibility to verify the statements of witnesses via either the surveillance system, if installed on the incident scene, or by checking the eligibility of witnesses by contacting the phone company. For the goal 2.1, it depends on the achievement of several sub-goals. Basically, depending on the context of the environment, we note different missions: “Establish communication with IR (Internal Resource) (Goal 2.1.1)” mission, “IR confirms mission (Goal 2.1.2)” mission and “Select IR (Goal 2.1.3)” mission.

Fig. 3.
figure 3

Abstract & concrete goals crisis system.

Full size image

Identify goal actions.

In this step, we select the actions to carry out to satisfy and realize a specific goal. The figure below shows the model that associates the concrete goals to actions (Fig. 4).

Fig. 4.
figure 4

Goal actions model.

Full size image

4.2 Definition Phase

The definition phase represents the agents and their organizational structure classified with levels, it also presents the actions to be assigned to agents under each level. This phase is intrinsically dependent on the modeling phase, since there is a back-and-forth process between the two phases. This process helps at recognizing actions associated to each agent level. The entities of this phase are described in the meta-model of Fig. 5.

Fig. 5.
figure 5

Definition phase metamodel.

Full size image

Define agents and their level.

In this step, agents are defined and are organized under the specified hierarchical structure of the expected system. We note two kinds of agents: Agent Manager and Elementary Agent. The Agent Manager is the top-level agent who is responsible of taking decisions and maintaining the relationships between agents. Whereas, the Elementary Agent is the lower-level agent who interacts directly with resources. In some cases, an agent manager may supervise other managers and elementary agents.

Referring to the example mentioned above. To initiate the crisis management process, we need different agents: Coordinator agent, Surveillance system, Phone Company, Internal resource manager that supervises First Aid worker and the super Observer. The Coordinator and Internal resource manager represent the “agent manager” that coordinates the sub-agents. These agents denote the “Elementary Agent” since they are directly interacting with the resources to get information (Fig. 6).

Fig. 6.
figure 6

Agent structure.

Full size image

Assign actions to agents.

In this step, we note the different actions that an agent will need to perform to accomplish its goal. An action is assigned to an agent if only it meets the following rules:

  • If an action belongs to a level, then there has to be an agent associated to it

  • An agent cannot comply with two actions of different levels

Figure 7 displays the assigning of the actions to agents of level 2 according to the CMS case study. The agent manger “Internal Resource Manager” possess two actions: “Mission analysis” and “Assign Internal Resource”. Indeed, it has as role to evaluate the crisis, and then sends the appropriate resource to scene. For the other agents, there are elementary agent that possess each one of them a unique action to be accomplished.

Fig. 7.
figure 7

Assign actions to agents of level 2.

Full size image

4.3 Modeling Phase

The modeling phase models the high-level description of the internal behavior of the agent’s action as well as the external behavior that defines the interaction between agents. There is an iterative process of three steps to model the behavior for each level i (where i >= 1) identified in the definition phase:

  1. 1.

    Model the internal behavior actions of level i

  2. 2.

    Assign actions to agents of level i + 1

  3. 3.

    Model the external behavior actions of level i

Model the internal behavior actions.

Modeling the internal behaviour is mainly based on the representation of the decisions and states in terms of transition state diagram, which is based on the profile that we have proposed in [16]. Let us take the example of “Assign Internal Resource” action described in Fig. 8.

Fig. 8.
figure 8

Internal behavior.

Full size image

Once the agent receives action “Assign Internal Resource”, he makes the decision to “send the resource to the scene crisis”. If he does not get any notification form IR (Internal Resource), he adds an extra time waiting for any information, if after that time he does not receive anything, he changes his behavior by contacting the super Observer agent. When all information gathered, he sends a report about IR.

Model the external behavior actions.

In the external behavior, we describe the interaction between an agent manager and its sub-agents across the communication interface. This interaction is represented by the activity diagram, which is designed to describe the organizational behavior. The Fig. 9 describes the interaction between the internal resource manager and its sub-agents: the first Aid worker and the Super Observer agent.

Fig. 9.
figure 9

External behavior.

Full size image

4.4 Verification Phase

In the verification phase, we verify the behavioral properties of the system throughout the model checking technique. The model checking technique starts with making a comparison between two descriptions of a system behavior, one is considered as the requirement and the other is considered as the actual design. Then it verifies the system by exploring the state space to determine if the system has satisfied a series of properties. This model provides a counter-example in case the model does not meet the specification [17].

The BECAMEDA’s verification phase proposes to translate the models designed in the modeling phase to the SMV model checker [18, 19], the system’s properties is then expressed with temporal logic formulas.

We have used the gNuSMV tool [20] to verify the temporal properties expressed in CTL (Computational Tree Logic) formulas [21]. The Fig. 10 presents an example of a formal verification of the following system properties:

Fig. 10.
figure 10

Properties expressed in CTL.

Full size image

SPEC AG ((EV = “Send Internal Resource”) - > AX EO = “Wait IR to arrive at location”)

When the agent takes the decision “Send Internal Resource”, he will be in the state to wait for internal resource to arrive at location.

SPEC AG ((EV = “Send Internal Resource”) - > AX EO = “Request an Update”)

When the agent takes the decision “Send Internal Resource”, he will be in the state to request an update

SPEC AG ((EV = “Send Internal Resource”) - > AF EO = “Request an Update”)

When the agent takes the decision “Send Internal Resource”, he will always in the future be in the state to request an update

SPEC AG ((EV = “Send Internal Resource”) - > EF EO = “Request an Update”)

When the agent takes the decision “Send Internal Resource”, he will in some point in the future be in the state to request an update.

5 Conclusion

In this paper, we have introduced a method called BECAMEDA for the specification and the verification of Multi-Agent System. This method is based on different processes that help understanding the system starting from goals identification that captures the system needs, and ending with a formal verification of the system properties. The process specifies four phases: identification, definition, modeling and verification. This approach uses model-checking technique to perform formal verification of the agents’ behavior.

In order to illustrate the specification and the verification aspect of the method, we have used a Crisis Management System, the case study was kept simple to make the concepts of the method clear enough. Thus, the method has been effectively applied to a realistic example, which allows understanding more the system and being able to prove its accuracy. For more details about the verification phase, the reader can refer to our previous works [18, 19].

As future work, we are currently investigating to combine the BECAMEDA method with an existing approach that considers in depth the designing phase. This will be an important extension of the BECAMDA method to build up a complete method that deals with the different MAS engineering phases.