1 Introduction

Agent systems are inherently complex distributed systems consist of agents that autonomously interact to each other in an environment to perform tasks and achieve goals [151]. Performing verification is important to detect violations of agents and the agent systems properties. Verification of agent systems is the process to check properties violations of agents complex systems. In general, the verification is performed by mapping the requirements of the agent systems into properties specifications that will be checked using verification techniques whether real system or system design model comply with the specified properties. The systems that meet or fulfill the specifications are classified as correct systems [41].

This paper reports the completed Systematic Literature Review (SLR) that explores the system verification techniques proposed so far and classifies as well as analyzes them. The objective of this review is to identify gap and future research direction in the area of agent systems verification. This study aims to identify existing verification techniques and the properties addressed by those techniques. The surveys of existing techniques for checking agents and the agent systems properties during design, development and runtime of agents and the agent systems lifecycle are presented. This paper also identifies what are the criteria for each agent systems property in which the checking rules (to decide properties violations) are based on. Search terms with relevant keywords were used to identify primary studies that relate to the topic of discussion classified based on the used techniques and the addressed properties.

Existing traditional literature reviews of agent systems verification research are mainly focusing on specific techniques and properties. In our study, we have performed an SLR to address sets of research questions in order to extract related information from the selected literatures. This SLR is intended to complement the traditional approach as its advantage is to give thorough state-of-the-art overview as compared to traditional literature review that provides an in-depth study, which is more specialized only toward certain techniques or properties. We performed an SLR on verification of agent systems published from 1995 to January 2017. In summary, the aim of this SLR is to provide wide overview and summary of (1) the existing agent systems verification techniques, (2) the agent systems life-cycle phases where the techniques have been implemented, and (3) the focused agents and agent systems properties. This SLR is intended to benefit agent systems designers, developers, and researchers from the industries and academia to understand the research pattern of agent systems verification practices and overcome the challenges.

The rest of the paper is structured as follows. Section 2 presents the existing reviews. Section 3 describes the SLR methodology. Next, Section 4 presents the SLR results, maps the surveyed techniques with the identified properties and discusses the SLR results. Finally, Section 5 explains the SLR findings, and Section 6 concludes the SLR.

2 Background and related works

System verification ensures that the system is developed according to user requirements and design specifications (building the system right). Typical systems verification techniques are formal verification and runtime verification. Formal verification methods use mathematical proofs to perform verification. There are two types of formal verification that are deductive reasoning and model checking. Deductive reasoning such as manual proof and theorem proving proves the correctness of a system using axioms and proof rules while model checking checks correctness of system with respect to its requirement specifications [185]. To perform verification using model checking, the system is modeled as a state transition graph while the requirements in the form of properties specifications are expressed in logic notation. The model of a system is checked automatically whether it satisfies the expressed properties [62].

The existing approaches to verify agents and agent systems properties have been reviewed in several works. Janssen [110] explored and discussed the general criteria to evaluate multi-agent systems models verification and the challenges encountered. Bordini et al. [41] discussed current issues in multi-agent systems development including verification using model checking and stressed out the importance of having verification tools that are specific for verifying multi-agent systems applications. a Al [1] compared the existing verification techniques for multi-agent systems that are formal, semi-formal, hybrid and conventional techniques. The paper also stated how the verification of multi-agent systems properties process should be executed and what the expected outcomes were.

Many existing reviews of multi-agent systems verification techniques have been focusing on testing approach. Góxmez-Sanz et al. [96] explained the testing techniques (via verification and debugging) of multi-agent systems that are parts of multi-agent systems development process to identify failures and to check whether the system satisfies requirements. Athanázio et al. [89] surveyed the testing and debugging approaches and evaluating them based on the strategies used such as black-box, white-box, progressive, regressive, and performance testing. Multi-level testing that are at agent level (agents functionality) and society level (cooperation and coordination) were also reviewed. Houhamdi [105] has performed a survey to analyze the existing approaches and challenges of multi-agent systems testing. Nguyen et al. [181] classified multi-agent systems testing works based on the supported testing levels that are unit, agent, integration, system, and acceptance levels. The techniques used were also classified into passive (simulation-based techniques) and active (structured testing) approaches [181]. Zamani [233] investigated the important criteria of multi-agent systems testing and performed an evaluation of existing testing methods. The paper has identified the testing criteria that were disregarded by most of the multi-agent systems testing methods in order to propose standard testing process. Moreno et al. [168] and [1] gave the overview of verifications for multi-agent systems properties as continuous activities such as unit test, module test, integration test, system or functional test, and acceptance test throughout the entire multi-agent systems life-cycle that include the requirement level, design level, and implementation level. Both works presented the multi-agent systems testing process based on V-Model [112] to classify relevant verification methods and tools as well as identifying multi-agent systems characteristics that have not been tested [168].

There are also reviews and classification of faults and properties violation in agent systems that could be detected during runtime verification. Potiron et al. [195] extends the existing faults classification (development faults, physical faults and interaction faults) by adding specific faults related to agents internal and external autonomous behavior. These faults should be considered by developers for specification in order for the faults to be detected and to implement fault tolerance [195]. Bijani and Robertson [35] performed review of the existing practices to detect confidentiality, integrity, availability, and accountability violations in open multi-agent systems.

The above mentioned works have performed reviews of existing approaches and techniques for verifying agent systems properties and the classification of faults and properties violations in agent systems. Majority of the reviews have been focusing on the testing techniques [89, 96, 105, 168, 181, 233] and only two surveys classified multi-agent systems faults and properties violations for detection [35, 195]. However, the existing verification works of multi-agent systems have been widely performed in every stage of agent systems life-cycle and implemented for multiple types of properties using various kinds of techniques and tools that need thorough surveys and further analysis. Therefore, there is a need for a more comprehensive and systematic literature review to see the pattern of publications in this area to recognize, classify, and map the verification techniques and agent systems properties addressed by researchers to date.

3 Systematic Literature Review (SLR) methodology

Systematic Literature Review (SLR) is defined by [122] as “a means of identifying, evaluating and interpreting all available research relevant to a particular research question, or topic area, or phenomenon of interest”. Basically, the main purpose of performing the SLR is to study the width and the depth of the researched topic. In other words, SLR is performed to identify the related properties of certain topic and to reveal what are the issues and problems in each element. Systematic mapping has been also introduced as part of SLR approach [122]. It is used to construct a visual summary or map of a structure of the types of literatures and the published results by categories. The mapping process has been previously performed by [4, 158] to classify literatures according to types of papers and published results. In this study, the mapping approach is used to identify the properties of multi-agent systems interaction and to categorize the existing works focusing on verifying those properties. The process flow diagram of the systematic mapping is shown in Fig. 1 and the detail of the process is explained in the following subsections.

Fig. 1
figure 1

Process flow of the systematic mapping

Full size image

3.1 Definition of review questions (Scope)

To perform research in this area and to propose a new solution, the existing literatures need to systematically reviewed to identify gap. Researches in the area of agent system verification comprised of three main contributions that are i) the objectives (outcomes) of the verification, ii) the verification techniques used, and iii) the agent or agent system properties being verified. The SLR research questions are defined with the purpose to extract the information of the above three contributions from the selected literatures. The information will be used to perform mapping and to construct visual summary that shows the relation between the three contributions mentioned above. Therefore, the research questions (scope) addressed in this review are:

  1. RQ1:

    What are the verification techniques used by each work?

  2. RQ2:

    During which life-cycle phases the techniques were intended to be used?

  3. RQ3:

    What are the objectives of the verification and what are the properties focused by each work?

  4. RQ4:

    What are the outcomes of the data extractions and classifications of the verification works?

3.2 Conduct searching for primary studies in the literatures

The search strategy utilized in this research consists of the process of deriving the search terms and executing the search process at the selected literature resources. Similar to the research questions, this searching process also should extract information related to verification objectives, used techniques, and focused properties in the area of agent systems. Agent systems are also referred as multi-agent systems in many literatures to reflect that there are many agents in a system. The process to derive the search strings includes:

  1. (a)

    Identifying the primary terms that are: “agent system” and “multi-agent system”.

  2. (b)

    Identifying the terms that are related to research questions. In this study we include the techniques that are normally used for verification in the search keywords that are: “verification”, “testing”, “debugging”, “monitoring”, “assessing”, “diagnosing”, and “detecting”.

  3. (c)

    Identifying the terms used for describing the research outcomes. The word “violations”, “correctness”, “faults”, “failure”, “error”, “anomaly”, “emergent”, “invalid”, and “unwanted” that are the outcomes for verification process are included.

  4. (d)

    Using of the Boolean OR to incorporate alternative technique names.

  5. (e)

    Using of the Boolean AND to link the major terms.

The resulting search terms are described as follows: (agent system OR multi-agent system) AND (verification OR testing OR debugging OR monitoring OR assessing OR diagnosing OR detecting) AND (violations OR correctness OR faults OR failure OR error OR anomaly OR emergent OR invalid OR unwanted). The manual search steps performed are presented below:

  1. Step1:

    Keyword search of the related journals such as Journal of Autonomous Agents and Multi-Agent Systems and Journal of Artificial Intelligence Research, SCOPUS, IEEE/IET Electronic Library (IEL), and ACM Digital Library (ACM DL), Inspec bibliographic databases using Serial Solutions Central Search.

  2. Step2:

    Google Scholar search using the same search strings with filter to search only in Engineering, Computer Science, and Mathematics

3.3 Selection of papers and searching additional papers (Relevant Papers)

The inclusion criteria covered the studies related to the techniques used for verification of agents and agent systems properties. The studies of verification that are not related to the verification of agents and agent systems properties are excluded. The inclusion and exclusion criteria as the basis to include and exclude the studies are listed below:

Inclusion:

  1. (i)

    Papers that match the search keywords and addressing the research questions

  2. (ii)

    Papers that explicitly propose techniques for verifying agents and agent systems properties

  3. (iii)

    Papers that explicitly focus on verifying of agents and agent systems properties

Exclusion:

  1. (i)

    Papers such as surveys and reviews that match the search keywords but only give general overview and do not focus on proposing solutions for agent systems verification

  2. (ii)

    Papers that focus on verification of properties of systems that are not agent-based or multi-agent systems.

3.4 Identifying the research pattern (Classification Scheme)

As this SLR aims to analyze the proposed solutions for agents and agent systems properties verifications, several classification steps have been identified. The information are classified based on the reported techniques, properties, life-cycle levels where the techniques would be implemented, and the verification goals either for checking properties satisfaction (correctness) or detecting properties violations (faults). This classification approach was chosen for the following purposes:

  1. (i)

    To analyze the existing works in the area of agent systems verification in order to identify the needs to extend the existing approaches and propose new contribution.

  2. (ii)

    To accomplish the objective that is to find gap and derive research direction.

  3. (iii)

    To report the number of existing works that have been focusing on certain techniques, properties and outcomes.

  4. (iv)

    To map, visually summarize and to identify which techniques have been largely used, for which properties and for what purposes.

Other alternative classification approaches may also be used such as classifications of the literatures based on the types of publications (journals, conferences, etc) or the types of works reported (methods, models, frameworks, case studies, etc). However, to analyze previous works for finding research gap, deriving research direction and proposing new contribution toward new techniques and identify new properties to be verified, the classifications need to be made according to the existing reported techniques, properties, life-cycle levels, and outcomes. Based on those reported works, the classifications need to be performed based on the patterns found when the data has been extracted from the selected literatures.

First, the selected papers are classified according to the types of verification techniques used for checking agents and agent systems properties. Second, the techniques are further classified into the agent systems life-cycle levels where the techniques were intended to be used. Third, the papers are classified based on agents and agent systems properties addressed in the papers. Fourth, the properties are grouped based on the verification approach or goals that are either to check properties satisfactions or to detect properties violations. Finally, the properties addressed in the papers were classified into agents and agent systems properties groups that are (i) system properties, (ii) agents internal properties, (iii) agents social properties, (iv) agents knowledge properties, and (v) agents interaction properties as detailed out below:

  1. (i)

    System properties include the overall correctness of the agent systems such as temporal properties, reachability, events sequence and concurrent properties.

  2. (ii)

    Agent internal properties include the behavior of agents actions, characteristics and capabilities as individual agents such as reactiveness, proactiveness and controllability.

  3. (iii)

    Agent social properties include agents social behavior among group of agents such as commitment, coordination and self-organizing.

  4. (iv)

    Agent knowledge properties include the properties related to agents cognitive or mental states such as belief, goal and epistemic properties.

  5. (v)

    Agent interaction properties include the correctness of the agents interaction protocol, language, message exchange, message sequence, message syntax and message content.

  6. (vi)

    Agent quality properties include non-functional requirements and constraints to protect and to ensure that the agents can be trusted such as security. safety, privacy, confidentiality and integrity.

3.5 Data extraction and mapping process (Systematic Map)

Data extraction is a stage performed in systematic reviews. It is the process of gathering relevant data from the selected resources. Figure 2 illustrates the data extraction, classification and mapping process flow. For this study, the data extracted include the techniques, properties, lifecycle levels and verification goal (outcomes). In order to perform the classification steps mentioned in the previous section, the information from the papers need to be extracted. The information are classified based on the techniques, the properties, the life-cycle levels where the techniques would be implemented, and the verification goals either for checking properties satisfaction (correctness) or detecting properties violations (faults). Finally, the properties groups and the techniques types are then mapped to summarize and see which techniques have been largely used and for which properties.

Fig. 2
figure 2

Data extraction, classification and mapping process flow

Full size image

4 Systematic literature review results

This section presents and discusses the findings of this review. Firstly, an overview of the selected studies are presented. Secondly, a detailed description of the findings of this review in line with the specified research questions are presented in separate sub-sections. Finally, the review results are also interpreted in this section, in the context of the research questions.

4.1 Overview of the searched and selected studies

Figure 3 shows the searching and selection process. During the first searching process, 358 papers were collected. After removing duplicates and applying the inclusion and exclusion criteria, the total of relevant papers were 193. Next, the second searching process of the papers cited by the previously selected papers was performed and 231 papers were collected.

Fig. 3
figure 3

Searching and selection process

Full size image

Figure 4 presents the number of works by year of publication. For the past two and half decades, lots of researches have been performed in the area of agent and agent system verification. From 2004 until January 2017, the number of publications are very high (ranging between 10 to above 25 papers) every year in which 2015 shows the highest number of publications. At this time while the paper is written, more publications are being published in the area of agent and agent system verification. The number of publications shows that agent system verification area is an active research area worth to be explored and studied.

Fig. 4
figure 4

Number of works by year of publications (1995-2017)

Full size image

The SLR processes include the identification of agent properties focused by researches, the identification of verification techniques used and the classifications of the techniques and the properties. From the classifications, research gap in the area of agent systems verification is identified and research direction is derived at the end of the SLR. The results of the process that answer each of the research questions are presented in the following subsections.

4.2 Identified verification techniques (RQ1)

From the selected 231 relevant papers, the techniques proposed and used by each paper were identified. Figure 5 shows number of works for each type of techniques used for checking agent properties. The techniques were grouped into 10 main types of verification techniques for easy analysis. The most popular technique is the model checking, formal method, or model-based verification technique as 44.04% (96) of the works use this type of techniques to verify agent and agent system properties. This is followed by the testing and debugging agent and agent system properties during development as 16.51% (36) of the works address this type of techniques to check agent and agent system properties. The next popular technique is the runtime verification as 9.17% (20) of the works choose this type of techniques.

Fig. 5
figure 5

Number of works proposing verification techniques

Full size image

Existing researches have achieved their objectives in addressing agent and agent system properties. Table below shows the existing achievements and limitations of verification techniques in addressing agent properties [38].

4.3 Classification of the techniques according to life-cycle levels (RQ2)

The techniques for verifying agent and agent system properties were proposed to be implemented during certain multi-agent systems and agent systems life-cycle phases. Three agent systems life-cycle levels were identified that are design level, development level and runtime level where the techniques are intended to be used as suggested by [24]. The techniques were classified into these three agent systems life-cycle levels. Percentages of the existing agent and agent system verification works implemented in those three levels are displayed in Fig. 6. Most of the verification activities were performed during design level (49%). It is followed by techniques that had been proposed to be implemented during development level (27%) and design level (25%).

Fig. 6
figure 6

Agent system verification implementation

Full size image

The techniques utilized in each level were identified. First, the techniques that were implemented during design are model checking, model-based verification, formal method, theorem proving, mathematical analysis and statistical analysis. Second, during development, testing, debugging and simulation techniques are used. Third, during runtime, model-based fault detection, fault/anomaly management, testing, debugging, runtime verification, execution checking and analysis using logical, statistical, empirical and artificial intelligence (AI) techniques are utilized. Figure 7 shows the techniques that have been implemented during each life-cycle phase.

Fig. 7
figure 7

The techniques implemented at different lifecycle levels

Full size image

Based on the above classification, the issues of agents and agent systems can be divided into three phases that are during design, during development and during runtime. During design, it is possible that there are design flaws such as deadlock, live-lock, underspecification, over-specification, and interaction protocol violations [2]. Since 1990s, many solutions have been proposed. One of them is by inventing tools e.g. MCMAS (model checker) [147] and SOCS-SI (automated theorem proving) [77] customized to perform formal verification on agents and agent systems during design time by considering common agent abstractions [24]. Another approach is by checking on selected critical smaller models extracted from the complex agents and agent systems and use general-purpose distributed model checking tools such as SPIN [104], UPPAAL [219], NuSMV [61] and PRISM [131] to verify against general properties such as temporal logic. Many research works have been done on agent and agent system verification during design using model checking. Benerecetti and Cimatti [32] have proposed the use of MATL (Multi-Agent Temporal Logic) and MAFSM (Multi-Agent Finite State Machine) for the specification of multi agent BDI (beliefs, desires, and intentions) properties and modeling of the multi agent system, respectively. Next, series of works performed by [40] extend the temporal specifications of agent properties with the agent behavior properties of BDI. The specifications are verified using Spin and later using Agent JPF (AJPF) model checker. Another work that supports the verification of BDI properties for multi-agent systems is MABLE [223], a multi agent programming language and model checking. Lomuscio et al. [147] developed model checker for multi-agent systems (MCMAS) that can verify time, knowledge, and behavior of agents. Similarly, MCK (Model Checking Knowledge) [87] is also developed to reason about temporal (time) and epistemic (knowledge) properties.

During development, developed agent systems need proper debugging and testing. Monitoring or debugging of agents and agent systems has been performed for individual and multi-agent levels. Individual agent testing and debugging can be accomplished using debugging and testing techniques, platforms or tools for the programming languages used to develop the agents such as JAVA using JADE platform [31] or AgentSpeak using Jason [38]. Multiple agents need debugging and testing that includes the preparation of test cases of agent behavior, knowledge, and interaction during development phase. For fewer number of agents (less than 100), interactions between agents can be monitored using existing agent platforms such as JADE. On the other hand, for higher number of agents, advanced high-level analysis such as data mining is performed toward the ACL messages using tools such as ACLAnalyser [45]. During runtime, agents interact with each other by sending request and response messages, distributing and publishing information to participate, contribute, or collaborate in agent community. Agent communication can be specified to follow multi agent standard interaction protocols specified by FIPA. In addition, to understand each other at the application level, a common ontology specifying languages and vocabulary used within the application has to be followed. As the system operations, environment, and user inputs evolve, there is a pressing need for verification during runtime [23].

During runtime, executed system can still suffer from properties violations during runtime due to external factors such as dynamic input and preferences from users, intruders, newly integrated software, or other agents from different platforms, hosts, networks, or environments (web services, Internet or wireless network). The issues include correctness of message structure (syntax), correctness of message content (ontologies), correctness of message sequence or conversation (interaction protocol), believability (trust toward the sender), confidentiality (role of the receiver), etc. Thus, besides verification during design, monitoring and verification during runtime are equally important to verify the correctness of agent communication. Interactions between agents from different hosts and platforms can be visualized using JADE RMA (Remote Monitoring Agent) graphical user interface (GUI). The produced sequence diagrams allow message sequence correctness to be checked and analyzed to certain level [31]. As agent system or multi-agent systems itself is a solution for critical problems for various kinds of social, business, and computer applications [215]. The verification of agent systems is exceptional from other systems [41]. Model checking agents can always be developed within the applications, alongside other agents in multi-agent systems to verify running processes. Model checking method called MCa (Model Checking Agent) [206] and MVA (Model Verification Agent) [207] have been developed to verify message passing properties such as byte, syntax, and time checking of SMS Management and RFID systems, respectively. Osman [185] introduced runtime verification for agent interactions that check agent deontic and trust models. Finally, [198] proposed a debugging process structure and the implementation of debugging agent to detect commonly found errors during multi-agent systems execution such as uninitialized agent, failure to send messages, wrong recipients, message sent multiple times, and wrong message sent. The proposed debugging agent monitors exchanged agent interaction messages and checks their correctness against interaction protocols [198].

4.4 Identified verification objectives and the focused agent properties (RQ3)

From the searched and selected relevant agent system verification literatures, the verification objectives for each paper are identified. The aims of the proposed verification solutions are classified into two main objectives that are 1) to check satisfaction of agent properties, and 2) to detect agent properties violations (faults). Based on these two objectives, the identified properties are classified into two large groups that are 1) the checked agent properties and 2) the detected properties violations (faults). Figure 8 shows the number of works that check satisfaction of the agent properties. The most popular properties are the temporal properties as 47 research works had been focusing to verify these properties. Next, 23 works for verifying epistemic properties had been performed, followed by agent safety (15 works), interaction protocol (12 works), liveness (12 works) and agent BDI properties (10 works). Other properties such as reachability (8 works) and security (8 works) are also significant in the area of agent systems verification.

Fig. 8
figure 8

Number of works that check satisfaction of agent properties

Full size image

Beside satisfaction or correctness checking of the properties, the verification activities also focused on detecting faults as shown in Fig. 9. Most faults detected are the interaction pattern and message sequence faults (14 works). Faults that are due to emergent or unexpected behaviors (13 works) and message exchange (10 works) are the next popular issues being focused by researchers. Belief-related faults (8 works), goal-related faults (7 works) and interaction protocol violations (6 works) also contributed to the number of faults detected during agent systems verification. The faults are also classified into 5 main groups that are agent system faults, agent internal faults, agent social faults, agent knowledge faults, and agent interaction faults. However, agent quality faults have yet to be detected.

Fig. 9
figure 9

Number of works that detect properties violations (faults)

Full size image

The classification of the properties extracted from the literatures is shown in Fig. 10. The properties are classified into six main properties groups that are the agent system properties, internal properties, social properties, knowledge properties, interaction properties, and quality properties. The classification was made based on the words mentioned or used in existing papers. This classification was intended to see the popularity of the properties addressed by existing works.

Fig. 10
figure 10

Properties checked by existing works

Full size image

Next, the agent properties are further classified into agent requirement categories that are agent functional and non-functional requirements [49, 232]. Figure 11 shows the agent properties classified under agent functional and non-functional properties. The agent functional properties are the properties that fulfill agent functional requirements and agent non-functional properties are the properties that should satisfy agent non-functional (quality) requirements.

Fig. 11
figure 11

Classification of agent properties based on agent requirement categories

Full size image

4.5 The mapping of the verification works classifications (RQ4)

The SLR results have presented the classification of verification techniques into several groups (RQ1), the classification of works into lifecycle where the techniques had been used (RQ2), and the classification of works into verification objectives and into categories of focused properties (RQ3). For RQ4, the outcomes of the approaches are classified into checked properties satisfactions and detected properties violations. The results of the categorization of the papers into verification outcomes and focused properties are included in Appendix A. Consequently, a map of verification techniques is developed with respect to the checked properties and detected properties violations (faults) as shown in Fig. 12. The map represents the visual summary of the mostly used techniques and the successfully checked properties and detected faults.

Fig. 12
figure 12

The map of number of verification techniques with respect to the number of checked agent properties and detected faults

Full size image

The results of the mapping show distribution of the number of works using certain techniques for checking agent properties or detecting faults. Large number of works had been dedicated to check properties during design (using model checking or model-based verification, theorem proving, mathematical analysis, and formal method) as compared to efforts to verify properties during development (using simulation, debugging, and testing) and runtime (fault or properties violations detection, fault management, debugging, testing, and runtime verification). It is obvious that the model checking or model-based verification techniques and formal methods have been the main focus of the researchers in this area as majority of the works had been addressing these techniques for the checking of agent properties (142 works). The debugging or testing techniques performed during development proposed to detect faults and properties violations of agent properties (40 works) are the second highest number of classified works. The third group is the runtime verification techniques used to check satisfactions of agent properties (21 works each). The mapping shows that the majority of the verification works are focusing on the checking of properties while fewer efforts are directed to detect faults or properties violations in agents and agent systems. The map also shows that there is an implementation gap for the purpose of detecting faults of agent quality properties.

5 SLR findings and research direction

Verification of agent and agent system properties is a huge topic as improvement of techniques are being proposed and new properties are being discovered form time to time. 231 primary studies were identified during the search process. From these studies, 49% were implemented for verification of agents and agent systems during design, 27% during development and 25% during runtime. The highest number of techniques used is the techniques are classified under formal method, model checking, and model-based verification techniques (44%) and followed by the testing and debugging during development (17%). The properties that are largely addressed by the selected studies are temporal properties (19%) and epistemic properties (9%). From this review, the findings are enlisted below:

  1. (i)

    This study has shown that verification of agent and agent system properties have been significantly discussed in agent system and multi-agent system domain. However, most existing agent and agent system verification works have been focusing on checking properties using model checking and formal method techniques that were implemented during design level. Many verification techniques also have been discovered in this study including verification techniques performed during execution that are model-based fault detection, fault management, debugging and testing during runtime, and runtime verification. Some of these techniques have not been reviewed in the existing multi-agent systems and agent systems verification surveys. In this SLR, the works implementing those techniques are classified as the verification performed during runtime. The applicability of new techniques for verifying and validating agents and agent systems properties during execution especially in open environment where agents can freely join or leave the systems still needs to be further explored.

  2. (ii)

    The importance of incorporating verification throughout the entire multi-agent systems or agent systems lifecycle is revealed. The classification of techniques shows that verification of agent and agent system properties have been performed not only during design to verify model and during development to test implementation, but also during runtime to verify agent and agent system execution properties. As compared to the design level, the number of agent and agent system verificationperformed during runtime is a lot lesser (refer to Figure 6). Thus, it might be the area that is worth to be explored by future researchers of agent systems verification.

  3. (iii)

    By classifying the properties into six groups (system, internal, social, knowledge, interaction, and quality), it is easier for future researchers to situate their works into these groups. In order to perform and improve verification of certain agent characteristics in the future, the properties mentioned in this SLR should be considered by researchers. This classification also shows gaps in certain area of agent systems that need to be covered in the future. The coverage issues of agent and agent system verification have been previously discussed by [165] and [188]. Thus, by considering all properties, it will hopefully improve the coverage of the agent and agent system verification. The classification of agent properties based on agent requirement categories that are functional and non-functional properties indicates that non-functional properties are the areas that need further research.

  4. (iv)

    The classification of the verification outcomes into checked properties satisfactions and detected properties violations (faults) also indicates that not many verification approaches focus to detect faults or properties violations (refer to Fig. 12). Bordini et al. [41] also stated that although agent applications has been verified to be correct, unpredictable emergent behavior can still occur due to agent reactiveness, proactiveness, flexibility, and social-ability characteristics. Thus, there is a need for future research to effectively identify agent properties violations such as faults and anomalies. From the mapping of the results, we identify that agent quality properties violations (faults) detection is yet to be explored. Some of the agent quality properties include safety, reliability, and trust.

  5. (v)

    The relation between agent properties depends on the functional and non-functional requirements of the agent systems. At the end of this study, some of the properties are compatible. For example, temporal properties and epistemic properties are always verified as the combination of temporal and epistemic properties using temporal-epistemic logic (Belardinelli, 2015). Next, there is also a research that combines epistemic with strategy properties (Belardinelli, 2017) and deontic with trust properties (Osman, 2008). Detail review can be performed to study the relation between agent properties.

6 Conclusion

This paper aims to review the outcomes of the existing agent systems verification works, the techniques used to verify agents and agent system, and the addressed properties. First, the verification outcomes are grouped into the checked properties satisfaction and the detected properties violations. Second, the used techniques are the techniques for verification during design, during development, and during runtime. Finally, the addressed properties are classified into the properties of the agent system itself, the agent internal properties, the agent social properties, the agent knowledge properties, the agent interaction properties, and the agent quality properties. The main contributions of this work are the classification and mapping of the existing works based on these verification outcomes, the used techniques and the addressed properties in Fig. 12. The objectives of this work that are to find implementation gap and future research directions have been accomplished.

The limitation of this study is that the techniques and properties are classified into groups in order to accomplish the objectives of the study. In the future, further analysis needs to be performed in order to identify relationship between those techniques and the verified properties. By identifying the relationship between the techniques and properties, a hierarchical relationship map, or proper taxonomy between the techniques and properties can be produced.