Using default logic for agent behavior testing

Abstract

An agent is an autonomous entity that can perform actions to achieve its goals. It acts in a dynamic environment that may engender failures regarding its behavior. Therefore, a formal testing/verification approach of the agent is required to ensure the correctness of its behavior. In this paper, we propose a Default Logic formalism to abstract an agent behavior as knowledge and reasoning rules, and to verify and test the consistency of the behavior. The considered agents are implemented with JADE framework. Also, agent abstraction is translated into Answer Set Programming and solved by Clingo to generate dynamic and adaptive test cases of the agent behavior. The dynamic test cases allow predicting the agent behavior when a new information arises in the system.

Keywords

Agent behavior multi-agent systems testing verification non-monotonic reasoning default logic

ï»¿

1. Introduction

Several distributed applications are now increasingly being designed as a set of autonomous and interactive agents. These sets of agents are named multi-agent systems (MAS). Several architectures, models and tools have been proposed to develop MAS and they have been applied to various application domains, such as medical monitoring, traffic control, UAV control and robotic.

For most multi-agent applications, it is necessary to ensure the correctness of their implementation before their deployment. To boost the success of MAS, it is important to develop verification solutions. The verification process includes checking of documents, design, code and programs whereas the validation process includes testing and validation of the actual product. To validate something such as a claim or statement, we have to prove or confirm that it is true or correct. During this process, the difference between the actual result and the expected result can be identified and corrective action can then be considered. Therefore, the verification finds the bugs early in the development cycle whereas testing finds the bugs that verification cannot catch in the case of agent behavior, especially when dealing with a false or an unknown information.

To deal with this testing issue, several testing methodologies have been proposed, some consider inferential models and model-based tests [14, 30] and others exploit genetic algorithms in the field of combinatorial tests [26, 28, 27]. Also, the most important consideration in testing a program is the design of the test scenarios [10]. However, creation and completeness of these scenarios cannot guarantee the absence of errors. The test scenarios are important, but the full coverage of the tests is almost impossible; an implemented test strategy tries to put as many full tests as possible. The key issue of testing is reached when the subsets of all the scenarios have a chance of detecting a wide coverage of the errors.

These methodologies are suitable for testing deterministic behaviors, i.e., behavior will move in the same direction continuously. Moreover, they consider that any fact is true or false. They don’t propose any solution to deal with unknown information and adaptive agent behavior. Agent behavior is not always based on classical logic. Non-monotonic reasoning provides a suitable solution to deal with unknown information and non-deterministic behavior.

Non-monotonic reasoning depends on knowledge and facts. It will change with the improvement of knowledge or facts which may be incomplete or unknown. Adding knowledge will invalidate the previous conclusions and change the result. Hence this reasoning is useful in a domain such as (MAS). Recently Mendez et al. [24] treat the errors related to the code branching conditions by injecting parameters into the code and find diverse inputs by perturbing the injected parameters. The created test suites are focused on specific program parts. But the treatment of unexpected situation facing to the handling of an unknown information is still an open issue.

To address this problem, we focus on the testing process, both on the code added/modified by the developer which requires adaptation of the tests (to suit a new situation), and the handling of information. This information may be false or unknown but it is necessary for the reasoning of the agent behavior. We propose to use the non-monotonic reasoning to build an abstraction of the agent behavior, especially the Default Logic (DL) [34], that is motivated by its capability to treat the unknown or incomplete information by describing the knowledge representation and default reasoning rules. An algorithm for constructing the agent theory (knowledge base and reasoning rules) in the form of Answer Set Programming (ASP)1 is provided. Then using it by Clingo solver2 which produces an abstraction of all possible paths as stable models. Another aspect that has not been treated in previous works is the adaptation of test cases at runtime. Thereby, we develop a complementary module that transforms models into test cases with disruptive values. Moreover, an implementation of the proposed approach is provided upon Jade framework [5]. It includes a module for capturing3 the agent behavior and applying an appropriate strategy about a real dynamic behavior at runtime.

The remainder of this paper is organized as follows. Section 2 presents the related work and highlights the open issues. Section 3 presents an overview of the preliminary definitions of Default Logic as well as some formulas that we have defined according to our context. Section 4 describes a conception of our solution, then a case study is proposed in Section 5. Section 6 concludes this paper and gives some future works.

2. Literature review

Very few works have been developed for verifying and testing MAS. Most of these works use Prolog or Petri Net formalisms [7, 35]. We distinguish two kinds of approaches: monotonic approach and non-monotonic approach. Unlike the monotonic approach, the non-monotonic approach deals with unexpected behaviors.

In the monotonic approach, the work of Roungroongsom and Pradubsuwun [35] is centered on verification in order to detect the safety and time constraint failures that may happen at design time. It relies on Time Petri Net as a tool to model the input verification. It observes a MAS runtime and collects the messages. The latter are then converted into a Time Petri Net. Briola et al. [7] propose a solution for Jade. This solution extends the Jade Sniffer agent for distributed runtime verification, which is dedicated to intercept the exchanged messages during the execution, and verifies the messages by a Prolog-based tool. It verifies that interactions are compliant with the agent interaction protocols, but it does not cover the exceptional scenarios inside the internal implemented agent behavior. The work of Lacey and Deloach [19] introduces a formal methodology, where the agent messages are converted into a model with Promela modeling language. That model is then analyzed by SPIN to check the correctness of interactions. Also, Lam and Barber [20] propose a tracing method and a tool to verify an expected agent behavior in a MAS. It captures runtime data as actual agent behavior and creates modeled interpretation in terms of agent concepts (e.g., Belief, Desire and Intention).

These works of the monotonic approach aim either verifying the interaction protocols or guiding debugging efforts. They consider that the test designer knows the whole list of behaviors. However, the adaptation of tests to unexpected behaviors remains an open issue.

In the non-monotonic approach, recent test and verification methods mainly focus on the logical formalism to design the correctness of the agent reasoning. Most of these methods apply model checking to context-aware multi-agent systems. In [33, 32], the authors propose a formal modeling of resource-bounded context-aware systems. They handle inconsistent context information using defeasible reasoning, by focusing on automated analysis and verification. A model checker is used to perform automated analysis of the system (the desirable properties are expressed as LTL formulas) and verify non-conflicting context information guarantees it provides.

Zhang et al. [23] analyze pervasive computing systems which use a context awareness and concurrent communication. They adopt a CSP like hierarchical modeling language to model desirable systems, which could be used to encode and verify system properties using existing model checking techniques. The verification is based on the PAT model checker [39] and it is applied to a health care case study. However, it is not clear whether the predefined rules are used in a non-monotonic way. Sama et al. [36] model and verify an adaptive context-aware behavior of mobile applications by the adaptation of finite state machine. They propose some algorithms that are used to automatically detect fault patterns. They detect adaptation faults by exploring the space constructed by all possible value assignments to context variables. Preuveneers and Berbers [31] use SPIN model checker to verify a smart home environment and discuss consistency in context-aware behavior. Their work consists of designing rules based on general observations and showing how these rules can be inconsistent and lead to undesirable system behavior.

Another category of non-monotonic methods rely on Answer Set Programming (ASP), such as reasoning about actions and changes [4, 18, 17]. They study agent interactions by reasoning about agent observations of the world and also about the knowledge of other agents. Burigana et al. [8] address the problem of reasoning in multi-Agent epistemic settings exploiting declarative programming techniques. In particular, they present a modeling multi-agent epistemic planning in ASP. Moreover, other works [2, 38] focus on describing and reasoning about truthfulness of agents using answer set programming. These works illustrate the knowledge of the observations on the actions and the normal agent behavior. Furthermore, they evaluate over time the statements made by agents against a set of observations. i.e., starting from a collection of observations about the word state or actions performed by it. Then ASP program computes the truthfulness of statements of agents overtime.

The different works of the non-monotonic approach propose promising solutions. However, they don’t propose any solution for testing agent behavior in presence of incomplete information. The agent often receives new information which may be unknown and it must reason even in the absence of information. Tester aims to interpret or provide a meaning for an obscure behavior which inner reasoning is otherwise undesirable or non-understandable by the human observer.

In our testing approach, we share the idea of Enoiu and Frasheri [12] that relies on an autonomous agent. It includes a test agent which is more adaptive than a test case. It is described as a dynamic entity that can decide who and what the software should execute at runtime rather than a test case which is defined at the design step. The proposed approach is thus promising. But it has not yet been implemented using available agent technologies such as Jade [5], MCMAS [21], Netlogo,4 SeSAm,5 …etc. The use of Default Logic to formalize the captured agent behavior is proposed in the next sections.

3. Formal preliminaries

This section introduces Default Logic and describes the proposed predicates used in the proposed testing approach.

3.1 Default logic

Definition 1 (The Default Theory [34, 3]). A Default Theory consists of two parts: a propositional theory and a set of non-standard inference rules referred to as defaults. The non-monotonicity of Default Logic is due to the role defaults play [34, 3]. Consider a theory ${\Delta}$ , a Default Logic ${\Delta}$ is a pair ${(W,D)}$ consisting of a set ${W}$ of predicate logic formulas (called the facts or axioms of ${\Delta}$ ) and a countable set $D$ of defaults. A default ${\delta}$ has the form:6

$\displaystyle\frac{\varphi:M\psi_{1}\cdots M\psi_{n}}{\gamma}$ (1)

where ${\varphi,\psi}_{1},\cdots,{\psi}_{n}$ and ${\gamma}$ are closed predicate logic formulas, and ${n>0}$ . The formula ${\varphi}$ is called the prerequisite, ${\psi}_{1},\cdots,{\psi}_{n}$ are the justifications, and ${\gamma}$ is the consequent or conclusion of ${\delta}$ .

Sometimes ${\varphi}$ is denoted by ${\textit{preq}(\delta)}$ , ${\psi}_{1},\cdots,{\psi}_{n}$ by ${\textit{just}(\delta)}$ , and ${\gamma}$ by ${\textit{consq}(\delta)}$ . For a set $D$ of defaults, ${\textit{consq}(D)}=\{\textit{consq}(\delta)|\delta\in D\}$ denotes the set of consequents of the defaults in $D$ [1].

A default rule $\delta$ represents that if $\varphi$ is provable, and if $\neg\psi_{1},\cdots,\neg\psi_{n}$ ; each element of the justifications set is not provable, then we by default assert that $\gamma$ is true. For a default theory $\Delta=<W,D>$ , the known facts about the world constitute $W$ , and a theory extended from $W$ by applying the default rules in $D$ is known as an extension of $\Delta$ , defined as follows:

Definition 2 (The Extension of Default Theory [34]). An extension is a superset of the basic information of the system that includes everything that may be inferred, either by classical logical rules or defaults. We call an extension of the defaults theory, the set of all the sentences that can be deduced from the axioms by classical inference or default rules. This construction is iterated until stabilization, an extension $E$ of the theory ${\Delta=<W,D>}$ is a set of formulas, iff

$\displaystyle E={\bigcup}_{i=(0,n)}{E}_{i}$ (2)

where

$E_{0}=Th(W),$

${\forall i,E_{i+1}=Th(E_{i}\cup\{\gamma/\delta=\frac{\varphi:\psi}{\gamma}\in D% ,\varphi\in E_{i},\neg\psi\not\in E_{i}\})}$

$Th(S)$ denotes the set of well-formed formulas provable from $S$ by propositional logic.

As Reiter’s corollary:

A closed default theory $<W,D>$ has an inconsistent extension iff $W$ is inconsistent.

If a closed default theory has an inconsistent extension then this is its only extension.

A default is called normal iff it has the from:

$\displaystyle\frac{\varphi:M\psi}{\psi}.$ (3)

Definition 3 (Operational Definition of Extensions [1]). For a given default theory $T=<W,D>$ . $\Pi$ is a finite or infinite sequence of defaults from $D$ without multiple occurrences, and the segment of $\Pi$ of length k denoted by $\Pi[k]$ .

$\displaystyle\Pi=(\delta_{0},\delta_{1}\ldots).$ (4)

$In(\Pi)$ and $\textit{Out}(\Pi)$ are an associate two sets of first-order formulas, for each sequence $\Pi$ :

$\displaystyle In(\Pi)=Th(W\cup\{\textit{consq}(\delta)\mid\delta\textit{ % occurs in }\Pi\}).$ (5) $\displaystyle\textit{Out}(\Pi)=\{\neg\psi\mid\psi\in\textit{ just}(\delta)% \textit{ for some }\delta\textit{ occurring in }\Pi\}.$ (6)

Thus, ${In(\Pi)}$ represents the current knowledge base after the defaults in ${In(\Pi)}$ have been applied. And ${\textit{Out}(\Pi)}$ collects formulas that should not become part of the current knowledge base even after subsequent application of other defaults.

$\Pi$ is called a process of $T$ iff $\delta$ is applicable to $In(\Pi[k])$ , for every k such that $\delta_{k}$ occurs in $\Pi$ . Given a process $\Pi$ of $T$ defined as follows [1]:

•

$\Pi$ is successful iff $In(\Pi)\cap\textit{Out}(\Pi)=\phi$ , otherwise it is failed.

•

$\Pi$ is closed iff every $\delta\in D$ that is applicable to $In(\Pi)$ already occurs in $\Pi$ . Closed processes correspond to the desired property of an extension E being closed under the application of defaults in $D$ .

Definition 4 (The prioritization of Default Theory (PDL) [6]). A theory ${\Delta=<W,D>}$ is a prioritized default theory if ${<W,D>}$ is a normal default theory and ${\prec}$ a strict partial order in ${(D)}$ . ${E}$ is a PDL-extension of ${\Gamma}$ iff there is a strict well ${\prec\prec}$ on ${(D)}$ which contains ${\prec}$ and generates ${E}$ .

Definition 5 (Answer Set Programming (ASP)). For the application of Default Logic, we use answer set programming (ASP). ASP [3] is a logic programming language under the answer set semantics [16]. A logic program ${\Pi}$ is a set of rules:

$\displaystyle c_{1}|\dot{\ldots}|c_{k}\leftarrow a_{1},\dot{\ldots},a_{m},% \textit{not }a_{m+1},\dot{\ldots},\textit{not }a_{n}$ (7)

where $c_{i}$ or $a_{i}$ represents a literal of propositional language7 and not is the negation as failure of literal. For a rule of the form Eq. (7), $\textit{head}(r)$ denotes $c_{1}|\dot{\ldots}|c_{k}$ and body denotes $a_{1},\dot{\ldots},a_{m},\textit{not }a_{m+1},\dot{\ldots},\textit{not }a_{n}$ .

The rule is called constraint if the $\textit{head}(r)$ is empty, and it is called a fact when the body is empty.

Consider a set of ground literals $P$ . $P$ is consistent if facts $a$ and $\neg a$ do not occur in $P$ . A program ${\Pi}$ is said to be consistent if it has an answer set. Otherwise, it is inconsistent.

3.2 Predicates used in testing agent behavior

We now present a concrete system to formalize an agent theory as DL [16] using ASP. We select this language because several efficient ASP solvers are available and it is used by several default reasoning approaches [9, 4, 13, 29, 37, 8, 17]. We thus use ASP to formalize the knowledge and reasoning of a captured software agent behavior (see Section 4) and a Clingo solver to generate all possible models. Let us describe some statement definitions.

1.
A capture statement about a literal $P$ is noted:

$\displaystyle\textit{capture}(P)$ (8)

where $P$ is of the form $\textit{name\_sb}(id)$ . The name_sb represents the name of the sub-behavior and $i d$ is its instance.
2.
A capture statement about a fluent literal $P$ is noted:

$\displaystyle\textit{captured}(P,R)$ (9)

where $R$ is a Boolean, and captured means that $P$ occurs and its state is $R$ . True means that $P$ has already terminates its execution with success, and false has not yet terminated (it is waiting for the response of another process).
3.
A statement holds and at about a fluent literal $P$ is of the form:

$\displaystyle\textit{holds}(P,S)$ (10) $\displaystyle\textit{at}(P,R,S)$ (11)

Respectively, we say $P$ holds at $S$ times if its value is true and $P$ has a state $R$ at $S$ times.
4.
The default is of the form

$\displaystyle\textit{default}(D,C,\textit{BODY})$ (12)

where $D$ is the name of default, $C$ is a fluent literal that represents the Consequent, and BODY is a collection of literals. A default says that if BODY holds then $C$ also holds. The BODY regroups the positive and negative literals, i.e., in the sense of Reiter’s default [34], it is the justification and prerequisite set of the form: $p_{1},\ldots,p_{m},\textit{not }p_{m+1},\dots,\textit{not }p_{n}$ .
5.
The applied default is represented by

$\displaystyle\textit{applied}(D)$ (13)

We say the default $D$ is applied.
6.
A knowledge base ( $K B$ ) is a tuple $<W,PD,AD>$ where:

–
World $W$ is a set of captures, each of the form Eqs (8) or (9)
–
Possible Defaults $P D$ is a collection of expressions of the form Eq. (12)
–
Applied Defaults $A D$ is a collection of expressions of the form Eq. (13)

For $P D$ and $A D$ definitions (see Section 4 for details).
7.
A $KB=<W,PD,AD>$ is consistent if:

–
$W$ and $A D$ are consistent.
–
$AD\subset PD$

This means that all Applied Defaults ( $A D$ ) have to be included in the description of Possible Defaults ( $P D$ ) and the conclusions of $A D$ must be consistent with $W$ .

4. The testing strategy

Software testing [25] is an activity that aims evaluating a part of program by verifying whether it produces the required output for a particular given input. The goal of testing is not to provide means for establishing whether the agent behavior is totally correct; testing is a pragmatic and cheap way of finding errors by executing some test. Tests rely on a set of test cases. A test case is a specification of some input $I$ and the corresponding expected $O$ . It fails when the output produced by running the agent program does not match $O$ .

This paper focuses on testing the behavior of a software agent. The behavior represents an agent task or function. It may be a simple behavior, a decision behavior or a knowledge-based behavior.

The assessment of an agent behavior is done by testing its sub-behaviors (denoted by sb) considered as unitary, which correspond to the small parts of the behavior to be tested. While each unit is tested according to the black box testing. In this way, the agent behavior can be tested and verified by adding or modifying information to cause an undesirable behavioral due to cycle changes.

4.1 Overview of the strategy process

Figure 1.

An overview diagram of the test strategy process.

The formulation of the test of agent behavior is related to the properties of the agent that are deemed essential and on which the test will be based. The behavior requirements must be formally specified as testing properties, as shown in Fig. 1, important steps are used to specify the agent behavior. a Fig. 2 describes different steps of the construction process of an agent theory in the appropriate format. Steps are as follows:

•

Step i (Before Running): the essential part of this step is the construction of an agent theory ${\Delta=<W,D>}$ which includes the knowledge base $W$ (as representation of the agent world, beliefs, etc.) and a set of defaults $D$ . A pair ${<W,D>}$ can be called respectively at this step Possible Worlds ( $P W$ ) and Possible Defaults ( $P D$ ).

•

Step ii (During Running): this step aims t construct the extended theory of agent behavior ${E^{\prime}=<W^{\prime},D^{\prime}>}$ . A pair ${<W^{\prime},\Delta^{\prime}>}$ can be called respectively a Real World representation ( $R W$ ) and Applied Defaults ( $A D$ ).

•

Step iii (After Running): the test and validation of the consistency of new knowledge, i.e., all consequents that are inserted in $W$ of the theory have to be consistent with the prerequisites of the agent theory. Also, the subsequent applied defaults must be included into the set of possible defaults ( ${AD\subset PD}$ ).

In both steps (i) and (ii), we must use the Capture, Decomposition and Transformation (CDT) module (as described in Section 4.3). It is developed in AspectJ8 and Java to capture, split and transform the agent behavior into exploitable properties.

Figure 2.

Activity diagram of a partial CDT process (for the corresponding Algorithm 1–3).

4.2 Formal definition of a behavior capture

To make the previous process less ambiguous, we transform the software agent behavior into logical form. As shown in Fig. 2, CDT transforms the input data of agent behavior description (Step i) into output data as sub-behaviors ( ${sb}_{s}$ ) and rule constraints. We denote CDT transformation from input X to output Y as: ${X\xrightarrow{\textit{cdt}}Y}$ .

The data description can be represented as a sequence of symbols from a particular alphabet. Without any loss of generality, let a behavior $B$ be decomposed into $sb_{s}$ assumes the following properties:

1.
Data decomposition: $\exists sb_{k},\forall sb_{i},sb_{j}:sb_{k}=sb_{i}+sb_{j}$
2.
Data composition: ${\forall sb_{j},sb_{j}+sb_{k}=sb_{i}:sb_{i}}$ - ${sb_{j}=sb_{k}\wedge sb_{i}}-{sb_{k}=sb_{j}}$
3.
Transitive composition: ${\forall sb_{i},sb_{i}\rightarrow sb_{i+1}\wedge sb_{i+1}\rightarrow sb_{i+2}:% sb_{i}\rightarrow sb_{i+2}}$

Data composition and decomposition simply assume that captured data can be combined or split, without any loss of information. The transitive composition ensures that the transition is established between $sb_{s}$ .
4.3 The behavior capture and decomposition

A part of the CDT module is responsible for the capture. Firstly, as detailed in Fig. 2, it captures the behavior of the software agent by defining the points and parts of code which are identified as the source of input data. Followed by the decomposition, it concerns a recursively splitting of the agent behavior into sub-behaviors ( ${sb}_{s}$ ) until it achieves a last $s b$ in each branch of the tree, where the obtained ${sb_{s}}$ are considered as an elementary unit of tests as cited in Algorithms 4.3 and 4.3. The decomposition implementation is based on the bridge design pattern between the composite and strategy design patterns [15]. In each splitting step, we apply an appropriate strategy to construct the theory as world and default ${<W,D>}$ theory.

: Spliterb Agent Behavior $sb_{s}$ set of sub-behavior as elementary b is leaf apply SimpleStrategy; [b is composite] print parent; call Decomposer(b);

: Decomposerbeh – Agent Composite Behavior true or false

c: childs in beh call Spliter(c) set Strategy.Edge();

However, the set of defaults $P D$ can be represented as an oriented graph G as shown in Fig. 3b to represent all possible ways of default application (i.e. connection between defaults). The creation process of $P D$ is shown in Algorithm 4.3 to construct models. It takes as input the theory of the agent conceived as data and rules, and produces all the satisfying possibilities of the answer set called models, as detailed in Fig. 2. Each model corresponds to the sequence of defaults as mentioned in Eq. (12).

: models Construct $\Pi$ ASP file $\Pi_{s}$ sets of subsequent of the defaults to be apply

m: models in satisfiable $\delta$ : defaults in m add ( $\Pi$ [i], $\delta$ ) $\Pi_{s}$

Each default is formally represented as ${d_{i}=<\textit{preq}_{i},\textit{just}_{i},\textit{consq}_{i}>}$ , where $\textit{preq}_{i},\textit{just}_{i},\textit{consq}_{i}$ correspond respectively to prerequisite, justification lists and consequent of defaults.

4.4 Construction of the agent extended theory

Figure 3.

Oriented graphs a.b.c

During the running step (see Step ii), the agent starts running its behavior with one of the created and chosen models $\Pi$ included in the returned set in Algorithm 4.3, and as detailed in Fig. 2.

As depicted in Fig. 3b and c, let be a default ${d_{i}}$ with ${<\textit{preq}_{i},\textit{just}_{i},\textit{consq}_{i}>}$ , if the default is applied, its ${\textit{consq}_{i}}$ becomes a prerequisite of ${d_{i+1}}$ . In other words, the prerequisite ${\textit{preq}_{i}}$ of ${d_{i}}$ is a consequent ${\textit{consq}_{i-1}}$ of the applied default ${d_{i-1}}$ .

Simply, the application of a default corresponds to a transition from state $S_{1}$ to state $S_{2}$ (see Fig. 3a) which implies a new information in state $S_{2}$ , i.e., update the agent world by a new observation of the world or evaluate an internal action as a new conviction. Formally, as shown in Fig. 3c, ${w_{1}\xrightarrow{d12}w_{2}}$ corresponds to the passage from world representation $w_{1}$ to the world representation $w_{2}$ when $d_{12}$ is applied by execution of some actions.

: Input and output setsAD set (In, Out) Sets

$\delta$ : defaults in $\Pi$ add (In [i], $\textit{consq}(\delta)$ ) add (Out [i], $\neg\textit{just}(\delta)$ ) (In, Out)

Also, during Step ii, CDT captures the AD and constructs the In and Out sets according to Eq. (13). Algorithm 3 shows the collection of the information gained by the application of the defaults in ${\Pi}$ and represents the current knowledge base after the defaults in ${In(\Pi)}$ have been applied. Also, ${\textit{Out}(\Pi)}$ represents the set of collection of formulas that should not turn out to be true. Thus, after a subsequent application of other defaults, this should not become part of the current knowledge base.

Once all the defaults included in $\Pi$ are all applied, then CDT verifies the subsequent of defaults in $\Pi$ , i.e., if $\Pi$ is the process of agent behavior theory. The verification process is described in Algorithms 3 and 3. Thus, if $\Pi$ is a successful process, we conclude that the new extension is consistent (knowledge base is consistent).

: Successful of defaults setIN and OUT setsIN list of the current knowledge base after the defaults in $\Pi$ have been applied.OUT list of formula that should not become part of the current knowledge base, true or false

$p:\textit{predictaes}$ in IN $\textit{OUT.contains}(p)$ false

: Process of defaults set $\Pi$ list of defaults true or false

$\delta$ : defaults in $\Pi$ add (preq, IN) add (not just, OUT) call Successful (IN, OUT)

4.5 Chaining and scheduling

Once the obtained list is in an exploitable state, it can be accompanied by a special configuration which determines the logic of sequencing or scheduling tests. Generally, a test of a component is simply conditioned by the inputs and judged by its outputs. But when we have a grouping of tests with a specific order, a new policy which consists of the ordering is imposed. Separating and scheduling consists in determining which are the input values that are appropriate for each subcomponent and what is the consequence of a sub-component among the group on the overall behavior. As indicated in Section 4.3, the captured sub-behavior is presented as the smallest sb. Chaining involves linking discrete sb together in a series, such that each result of each sb is both the reinforcement (or consequence) for the previous sb, and the stimuli (or antecedent) for the next sb.

There are many ways to test chaining, such as (i) forward chaining: starting from the first behavior in the chain, (ii) backwards chaining: starting from the last behavior, and (iii) total task chaining: in which the entire behavior is tested from the beginning to the end, rather than as a series of steps. As a simple example, we consider the different actions of opening a locked door, first the key is inserted, then turned, then the door opened. Table 1 shows the level of testing actions. Consider the following actions:

•
a1 $=$ insert the key $\rightarrow\textit{state}(\textit{inserted})$
•
a2 $=$ trun the key $\rightarrow\textit{state}(\textit{turned})$
•
a3 $=$ push the door $\rightarrow\textit{state}(\textit{pushed})$

which correspond to the following states: inserted, turned and pushed.

Table 1
Level of testing actions

Action Insert Turn Push

1. Forward chaining Test Next Next

2. Backward chaining Previous Test Next

3. Backward chaining Previous Previous Test

4. Forward chaining Test Test Next

5. Backward chaining Previous Test Test

6. Total task chaining Test Test Test

On Table 1, we see on the first line, the insert action is considered as the test subject and turning and pushing are the actions that follow. Once that is tested, the subject is to test it turn, then opens the door as the next step. Then push the door is considered as the subject of test and the insert and turn are taken as previous actions. Once the first step is mastered, the entire task is tested individually. Finally, total task chaining would involve testing the entire task as a single series, prompting through all steps. But before that (line 6), we also test two actions as one unit (line 4 or line 5); insert and turn as the entire test subject and push as the action following it. Or turn and push as a whole test unit and insert as an action before it. For each sub-behavior test in the chain, we would induce disrupting elements at each level of the chain.
4.6 Adaptive test sequences

Action	Insert	Turn	Push
1. Forward chaining	Test	Next	Next
2. Backward chaining	Previous	Test	Next
3. Backward chaining	Previous	Previous	Test
4. Forward chaining	Test	Test	Next
5. Backward chaining	Previous	Test	Test
6. Total task chaining	Test	Test	Test

Usually, the test case suite is created at the design stage and has a static character, and any change requires manual intervention by the developer. We evolved this by making it more dynamic to the execution context and adaptive to the change in the code of the software agent. i.e., if description of the agent behavior changes, the CDT captures the new program code and regenerates automatically another list of inputs more appropriate for the implemented behavior.

Given the agent program $A P$ , and a sub-behavior node $\textit{sbN}\in AP$ , CDT captures the $A P$ and generates all execution paths that are used as models to generate scenario of test sequences. These inputs test set normally corresponds to a successful scenario. For any change in $A P$ by the developer, the module adapts the $T C$ and regenerates a new inputs test set. When the agent begins its execution, on the one hand, the module is responsible for capturing the execution state of all the sbN as mentioned in Section 4.3.

The $I n$ data of $T C$ relies on sbN for the description of agent behavior. Specifically, the $I n$ contains sbN constraints which is used by Clingo solver to generates an answer set as stable models. The set is transformed into test sequences and considered as successful running. A manual modification in parameter file allows a possibility to a specific configuration about names and constraints of rules.

The test case constructed in this step is based on the path search of nodes connection and the real execution for them. However, with a received messages from another agent, at runtime, information will be added into the knowledge base ( $K B$ ) of agent and the default becomes as follows: $\frac{A:C[a_{1},\dots,a_{n},\textit{msg}_{1},\dots,\textit{msg}_{m}]}{C}$ . The scenario will be extended and includes an exchanged message, this option is not treated in this paper but it will be done very soon.

In order to disrupt the agent behavior, the CDT module decomposes the behavior and retrieves all the connections and the order between sub-behaviors. At this step, the process is based on the created models as satisfiable and the CDT looks for all the inputs that lead the behavior to the unwanted goal. The CDT applies the principle of reinforcement to strengthen the behavior towards failure. It disrupts each sub-behavior in the chain and tests the failed case.

As indicated in Algorithm 4.3, Clingo solver generates answers set as stable models with length $L$ of models $M$ . a result corresponds to a list of models, each model is transformed to ${\Pi_{i}}$ , that elements are a subsequent of default ${\delta_{i},\delta_{i+1},\ldots}$ . Formally, for each ${\Pi_{i}}$ we have $k$ elements of ${\delta}$ denoted by ${\Pi_{i}[k]}$ . Suppose that $M_{1}$ contains $n$ defaults ${d_{1}\dots d_{n}}$ , and $M_{2}$ contains $m$ defaults ${d_{1}\dots d_{m}}$ , and $M_{L}$ contains $k$ defaults ${d_{1}\dots d_{k}}$ . a function of generating test sequence returns: $L$ case of normal test cases ( $T C$ ) and ( $3(n+m+\ldots+k)-2L$ ) of disrupted test cases (dTC).

4.7 A consistency test

To show inconsistency in the knowledge base, by so-called defeated tests, Algorithms 3 and 3 show implemented methods, where $\Pi$ is not process if there exists at least a default $\delta_{i}$ that is not applicable.

Formally as depicted in Fig. 4, a transition from $S1$ to $S2$ taken with performing an action $a_{1}$ is when the $E_{1}$ occurred and the condition $\neg J$ is satisfied. i.e., the transition taken with applying a default $d_{1}$ and $C$ is consistent with $P$ and no presence of $J$ . Otherwise, the transition from $S_{1}$ to $S_{2}$ is not taken when the condition $\neg J$ is satisfied and the test has failed.

Figure 4.

A consistency transition.

Three predicates are defined to conclude the state of the termination of the agent’s behavior: stable, disrupted or abnormal. If the agent is constructive with the new information, it must be finished in stable state. Otherwise, if it finished in conflict then the state is fixed to disrupted, i.e., the interaction has effect upon the behavior of agent. An additional state is added for the case of the occurring of an unexplained situation and it is labeled an abnormal state.

Let’s now some ASP rules, the Eq. (14) means that the agent $A G$ performs a sub-behavior $P$ , i.e., $\textit{captured}(P,R)$ . So, if the agent behavior $A G$ is stable at time $T$ and there is no evidence that $A G$ became false at time $T+1$ then $A G$ was true at time $T+1$ .

$\displaystyle\textit{stable}(AG,T+1):-\textit{stable}(AG,T),at(P,R,T),\textit{% not }\neg\textit{ stable}(AG,T+1).$ (14)

The Eq. (15) means that agent is stable at time $T$ and a behavior is captured but it is not holding at time $T+1$ , thus the execution is failed. The rule in Eq. (16) assume that at the same time it is abnormal that the agent realizes an action and its contrary.

$\displaystyle\textit{disrupted}(AG,T+1):-\textit{stable}(AG,T),\textit{% captured}(P,R),\neg\textit{ holds}(P,T+1).$ (15) $\displaystyle\textit{abnormal}(AG,T+1):-\textit{stable}(AG,T),\textit{holds}(% \neg P,T+1),\textit{holds}(P,T+1).$ (16)

Otherwise, it always remains a mystery when we cannot prove the state of the behavior if it is stable or disrupted therefore remains unknown. It is represented by the rule in Eq. (17).

$\displaystyle\textit{unknown}(AG,T):-\textit{not stable}(AG,T),\textit{not % disrupted}(AG,T).$ (17)

5. Case studies

To illustrate the proposed testing approach, we consider the examples used in [38, 2]. In these examples, the formalization of knowledge is carried out in the framework based on reasoning about agent beliefs and truthfulness.

5.1 Example 1

A Person X is walking in a good area of the city when suddenly another person Y appears and carries a knife walking towards him. So, X is afraid and he decides to defend, X person shoots the Y person hardly and that causes his death to the latter. When the police arrived, they started their investigation and they were faced with the following situations:

1.
Is the case manslaughter? During the confrontation punches went off and they caused the death of Y.
2.
Is the case an intentional homicide? This case is classified as self-defense despite the death.

During the investigation the police realize that the knife is fake. However, the question that arises is whether the culprit was aware or not? In this example, we demonstrate that the arise of a new information leads to contradictory knowledge.

To present a demonstration of our approach on the JADE framework, the developer will code it in a sequential behavior type as shown in Fig. 5, which will generate a single program $\Pi$ and the perturbation goes over the number of sub-behaviors as indicated in Line 1 of Table 2.

As described in Section 4, this will give us the results of generated defaults as detailed in the following.

$\displaystyle D=\left\{\delta_{0}=\frac{\textit{true:}}{\textit{walking}},{% \delta_{1}=\frac{\textit{walking:inImmentDanger}[\textit{knife}]}{\textit{% inImmentDanger}}},\right.$ $\displaystyle{\delta_{2}=\frac{\textit{inImminentDanger:onTrial}[\textit{% victim}]}{\textit{onTrial}}},{\delta_{3}=\frac{\textit{onTrial:guilty}[\textit% {victim}\wedge\textit{menacing}]}{\textit{inPrison}}},$ $\displaystyle\left.{\delta_{4}=\frac{\textit{inPrison:}[\textit{% servedthePrisonSentence}]}{\textit{inFreedom}}}\right\}.$

Table 2
A nominal and disruptive Test Cases ( $T C$ and dTC)

Line Test cases Disrupted test cases

$1$ $\Pi_{1}=(\delta_{0},\delta_{1},\delta_{2},\delta_{3},\delta_{4}).$ $\Pi_{11}=(\delta_{0t},\delta_{1},\delta_{2},\delta_{3},\delta_{4}).$

$\Pi_{12}=(\delta_{0},\delta_{1t},\delta_{2},\delta_{3},\delta_{4}).$

$\Pi_{13}=(\delta_{0},\delta_{1},\delta_{2t},\delta_{3},\delta_{4}).$

$\Pi_{14}=(\delta_{0},\delta_{1},\delta_{2},\delta_{3t},\delta_{4}).$

$\Pi_{15}=(\delta_{0},\delta_{1},\delta_{2},\delta_{3},\delta_{4t}).$

$2$ $\Pi_{2}=(\delta_{0},\delta_{1},\delta_{2},\delta_{6}).$ $\Pi_{21}=(\delta_{0t},\delta_{1},\delta_{2},\delta_{6}).$

$\Pi_{22}=(\delta_{0},\delta_{1t},\delta_{2},\delta_{6}).$

$\Pi_{23}=(\delta_{0},\delta_{1},\delta_{2t},\delta_{6}).$

$\Pi_{24}=(\delta_{0},\delta_{1},\delta_{2},\delta_{6t}).$

$3$ $\Pi_{3}=(\delta_{0},\delta_{5}).$ $\Pi_{31}=(\delta_{0t},\delta_{5}).$

$\Pi_{32}=(\delta_{0},\delta_{5t}).$

Figure 5.
State diagram of the sequential behavior of the man in imminent danger.

However, to make the example more interesting for the demonstration, we encoded it as Finite State Machine (FSM) type as depicted in Fig. 6. It is composed of five states except initial and final states. As described in Section 4, the generation of $\Pi$ is adaptive to the change of the code. This will give us the results of generated defaults as described in the following.

$\displaystyle D=\left\{\delta_{0}=\frac{\textit{true:}}{\textit{walking}},{% \delta_{1}=\frac{\textit{walking:inImmentDanger}[\textit{knife}]}{\textit{% inImmentDanger}}},\right.$ $\displaystyle{\delta_{2}=\frac{\textit{inImminentDanger:onTrial}[\textit{% victim}]}{\textit{onTrial}}},{\delta_{3}=\frac{\textit{onTrial:guilty}[\textit% {victim}\wedge\textit{menacing}]}{\textit{inPrison}}},$ $\displaystyle{\delta_{4}=\frac{\textit{inPrison:}}{\textit{inFreedom}}},{% \delta_{5}=\frac{\textit{walking:}\neg\textit{menacing}}{\textit{inFreedom}}},% {\delta_{61}=\frac{\textit{onTrial:victim}\wedge\neg\textit{menacing}}{\textit% {inFreedom}}},$ $\displaystyle\left.\delta_{62}=\frac{\textit{onTrial:}\neg\textit{victim}}{% \textit{inFreedom}}\right\}$

For the set $D$ , the CDT generates three paths as $P D$ . Let’s choose as an example the first case (line 1) of Table 2 and show the result for each step of disruption in Table 3. At each line of Table 3, we show the disrupted default name in the second column, then the possibility of its application or not in column 3. The columns 4 and 5 depict respectively the execution state of behavior and the consistency of its knowledge.

Table 3
Running of the selected dTC

Line Disruption Application Failure Consistency

1 ${\delta_{1}}$ $\delta_{5},\neg\delta_{1}$ Y Y

2 ${\delta_{2}}$ $\delta_{1},\neg\delta_{2}$ N Y

$3_{1}$ ${\delta_{3}}$ $\delta_{1},\delta_{2},\neg\delta_{3},$

$\delta_{5},\delta_{6_{1}}$ N N

$3_{2}$ ${\delta_{3}}$ $\delta_{1},\delta_{2},\neg\delta_{3},$

$\delta_{5},\delta_{6_{2}}$ N N

$4_{1}$ ${\delta_{6}}$ $\delta_{1},\delta_{2},\neg\delta_{6}$ Y N

$4_{2}$ ${\delta_{6}}$ $\delta_{1},\delta_{2},\neg\delta_{6},$

$\delta_{3},\delta_{4}$ N N

$4_{3}$ ${\delta_{6}}$ $\delta_{1},\delta_{2},\neg\delta_{6},$

$\delta_{3},\delta_{4}$ N N

Figure 6.
State diagram of the FSM behavior of the man in an imminent danger.

The first line indicates when we disrupt the sb (inImminentDanger). We observe $\delta_{5}$ becoming applicable (another path of execution) and not $\delta_{1}$ . In this case we conclude that the program continues it execution with success and the knowledge base is consistent. It is the same for the second case, when disrupt onTrial we observe $\delta_{1}$ is applied and not $\delta_{2}$ , but the program fails with consistency knowledge.

However, in line 3 when we disrupt $\delta_{3}$ , we remark a successful execution with inconsistent knowledge because the presence of proposition $\textit{inImminentDanger}\wedge\neg\textit{inImminentDanger}$ . Either there is a victim and there is no menacing danger which contradicts $\delta_{1}$ . $\neg\textit{imminentDanger}$ leads to both $\delta_{5}$ and $\delta_{6}$ becoming applicable. In this case, we conclude that, if $X$ had not yet noticed that the knife was fake at $\delta_{1}$ , we could accept the conclusion that at that time $X$ is believed to be in imminent danger. Otherwise if, $X$ shot $Y$ after observing that the knife was fake, we could accept the conclusion at $\delta_{1}$ time, that $X$ did not believe to be in imminent danger, so $X$ is guilty and so forth for the remaining cases.
5.2 Example 2 (MITM)

Line	Test cases	Disrupted test cases
$1$	$\Pi_{1}=(\delta_{0},\delta_{1},\delta_{2},\delta_{3},\delta_{4}).$	$\Pi_{11}=(\delta_{0t},\delta_{1},\delta_{2},\delta_{3},\delta_{4}).$
		$\Pi_{12}=(\delta_{0},\delta_{1t},\delta_{2},\delta_{3},\delta_{4}).$
		$\Pi_{13}=(\delta_{0},\delta_{1},\delta_{2t},\delta_{3},\delta_{4}).$
		$\Pi_{14}=(\delta_{0},\delta_{1},\delta_{2},\delta_{3t},\delta_{4}).$
		$\Pi_{15}=(\delta_{0},\delta_{1},\delta_{2},\delta_{3},\delta_{4t}).$
$2$	$\Pi_{2}=(\delta_{0},\delta_{1},\delta_{2},\delta_{6}).$	$\Pi_{21}=(\delta_{0t},\delta_{1},\delta_{2},\delta_{6}).$
		$\Pi_{22}=(\delta_{0},\delta_{1t},\delta_{2},\delta_{6}).$
		$\Pi_{23}=(\delta_{0},\delta_{1},\delta_{2t},\delta_{6}).$
		$\Pi_{24}=(\delta_{0},\delta_{1},\delta_{2},\delta_{6t}).$
$3$	$\Pi_{3}=(\delta_{0},\delta_{5}).$	$\Pi_{31}=(\delta_{0t},\delta_{5}).$
		$\Pi_{32}=(\delta_{0},\delta_{5t}).$

Line	Disruption	Application	Failure	Consistency
1	${\delta_{1}}$	$\delta_{5},\neg\delta_{1}$	Y	Y
2	${\delta_{2}}$	$\delta_{1},\neg\delta_{2}$	N	Y
$3_{1}$	${\delta_{3}}$	$\delta_{1},\delta_{2},\neg\delta_{3},$
		$\delta_{5},\delta_{6_{1}}$	N	N
$3_{2}$	${\delta_{3}}$	$\delta_{1},\delta_{2},\neg\delta_{3},$
		$\delta_{5},\delta_{6_{2}}$	N	N
$4_{1}$	${\delta_{6}}$	$\delta_{1},\delta_{2},\neg\delta_{6}$	Y	N
$4_{2}$	${\delta_{6}}$	$\delta_{1},\delta_{2},\neg\delta_{6},$
		$\delta_{3},\delta_{4}$	N	N
$4_{3}$	${\delta_{6}}$	$\delta_{1},\delta_{2},\neg\delta_{6},$
		$\delta_{3},\delta_{4}$	N	N

An interesting application of our approach is the detection of Man-in-the-Middle (MITM) attacks targeting computer and cyber-physical systems. The principle of an attacker is to become embedded between two communicating parties and to capture the exchanged messages. Once possession of the information is achieved, it can exploit it in an undesirable way. For example, we consider pushing the system to a crash by modifying the data or simply stealing secret information. This kind of attack has already been used on the Stuxnet9 system, targeting a specific industrial model which is the programmable logic controller (PLC).

Figure 7.

The state diagram of the FSM behavior of the MITM example.

Figure 7 describes the formalization of the states and transitions of the MITM example. In the same way as the preceding example, the defaults obtained from this are as follows:

$\displaystyle D=\left\{\delta_{0}=\frac{\textit{true:}}{\neg\textit{hot\_room}% },{\delta_{1}=\frac{\neg\textit{hot\_room:}[\textit{alert}]}{\textit{hot\_room% }}},\right.$ $\displaystyle\left.\delta_{2}=\frac{\textit{hot\_room:}[\textit{cold}]}{\neg% \textit{hot\_room}},{\delta_{3}=\frac{\textit{hot\_room:}[\textit{alert}]}{% \textit{overheat}}}\right\}$

When we apply the dTC to some program $\Pi$ , we disrupt $\delta_{2}$ and $\delta_{3}$ , i.e., we modify the cold and alert values at the same time. We conclude the transitions to overheat and $\neg\textit{hot\_room}$ states (both of the defaults are applied) and which represents an inconsistency of knowledge.

The alert condition leads to hot_room state then overheat state if it is still true. The cold leads to not_hot_room, cold and not alert lead to the same state. Although the alert is triggered, the climate indicator still indicates a cold state, which explains an inconsistency somewhere. This leads us to see the problem that can occur on the system and to think that either the warning indicator is defective (it was triggered for no reason), or the temperature sensor does not work anymore and indicates false values. Therefore, we add the default indicated by the dashed arrow in Fig. 7 that can represent an attack or an intrusion on the system.

5.3 Discussion

Through the two examples used in this section, we succeeded in illustrating our approach, we managed to predict some exceptions by the disruptive test sequence. In the first example, Balduccini et al. [2] and Son et al. [38] solved the problem of the diversion of fake knife to prove the innocence of the person $X$ by the inclusion of the priority operator (prefer) between defaults. In the second example and in the same way, they added a default that describes an inconsistency to represent an attack on the system.

However, the authors presented a solution to an already produced and detected problem. An interesting question is how does the developer come to see a problem that it’s not yet produced at a very early stage by testing?

6. Conclusion

The paper proposed a new testing approach based on adaptive test cases as well as the handling of false or unknown information. This approach uses the Default Logic formalism to abstract a software agent as default reasoning. The agent behavior is disrupted through default theory justifications. The latter correspond to the code transition conditions and use a Clingo to find an inconsistency in the knowledge base of the agent by disrupting the injected parameters. The testing approach does not only cover the errors that are visible in the code, such as the classic errors related to the code branching conditions. Thereby, it helps the Jade developers to improve their code at an early stage when some information is false or unknown, and to better identify the undesirable situations that may arise at any time. The approach has also been used to demonstrate how a software agent behavior upon Jade framework can be abstracted on the Default Logic (in the form of ASP) for building agent-based testing.

To validate the testing approach, we apply it to two examples. Through these examples, we were able to foresee some exceptions by the disrupting the test sequence. The results show that the approach is able to cover a desired test case face to the modifications in the code of the jade agent behavior. Moreover, adding the translating code into ASP improves the test vision and the failure detection, especially, when handling false and unknown (absent) information, and the ability to forecast a scenario that prevents the undesirable situation.

To improve our approach, we plan to expand the field of justifications set which defines an area of defaults that can be inserted or retired according to the evolving conviction. It consists of a set of default justifications. Thus, we will analyze the sub-behavior as a white box testing to conclude all justifications set of default theory. For this, we can totally or partially disrupt the agent behavior, in order to show the risk level of failure.

Moreover, in the proposed approach, the behavior of the agent is tested against its sub-behaviors according to black box testing. It should be interesting to consider the different message exchanges with other agents, in order to improve goal achievement, or affect the agent and prevent it from normal reasoning. By adding the messages into the default rules [11], we will be able to widen the field of justification, and treat the received messages as false, absent or unknown information. And in this case, the tests will be considered as a partial white box testing.

Footnotes

Answer Set Programming is a recent paradigm covering different kinds of logical programming, and their semantics is described by [].

https://potassco.org/.

https://www.eclipse.org/lists/aspectj-users/.

https://ccl.northwestern.edu/netlogo/index.shtml.

http://www.simsesam.de/.

$M$ is to be read as “it is consistent to assume”.

Rules with variables are viewed as shorthand for the set of their ground instances.

https://www.eclipse.org/aspectj/.

https://en.wikipedia.org/wiki/Stuxnet.

Author’s bios

	Djamel DOUHA is a lecturer in computer science at the university of Batna 2, Algeria. He received his master in computer science from University of Sciences and Technology Houari-Boumédiène (USTHB) in Algeria and he is preparing his PhD at USTHB in Artificial Intelligence.
	Aicha MOKHTARI is a Professor of Computer Science at the University of Sciences and Technology Houari Boumediène (USTHB, Algeria). Her research focuses on reasoning about knowledge and uncertainty, and its applications to access control, web semantic, distributed computing and ambient systems. Her work lies at the boundary of a number of fields. She usually teaches databases in an undergraduate course and knowledge representation and reasoning in a postgraduate course.
	Zahia GUESSOUM is Associate Professor at the University of Reims Champagne-Ardenne. She received her doctorship/PhD (1996) and then her “habilitation à diriger des recherches” (2003), both in computer science and from University Pierre & Marie Curie (Paris 6), France. She is the header of the MODECO Team of “Centre de Recherche en STIC” (CReSTIC) at the University of Reims Champagne-Ardenne. Her general research interests are about adaptive agents and multi-agent systems, fault-tolerant MAS, multi-agent oriented software engineering and coordination mechanisms. She authors more than 120 journal and conference papers in the fields of AI and multi-agent systems.

Yasser Moussa BERGHOUT is a lecturer at the Higher School of Commerce, Kolea, Algeria. He received PhD in computer science and Artificial Intelligence at the University of Biskra, Algeria. His current research focuses on Distributed Artificial Intelligence, Uncertainty Models, and the application of Artificial Intelligence in Finance.

References

Antoniou

, A tutorial on default reasoning, Knowledge Engineering Review 13(3) (1998), 225–246.

Balduccini

Gelfond

Pontelli

and Son

T.C.

, An Answer Set Programming Framework for Reasoning about Agents’ Beliefs and Truthfulness of Statements, 2020, 69–78.

Baral

, Knowledge representation, reasoning and declarative problem solving with Answer sets 1, Knowledge Creation Diffusion Utilization, 2001.

Baral

Gelfond

Son

T.C.

and Pontelli

, Using answer set programming to model multi-agent scenarios involving agents’ knowledge about other’s knowledge, in: Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol. 1, 2010, pp. 259–266.

Bellifemine

Poggi

and Rimassa

, Developing Multi-Agent Systems with JADE, 2001, 216–217.

Brewka

and Eiter

, Prioritizing default logic, in: Intellectics and Computational Logic, Springer, 2000, pp. 27–45.

Briola

Mascardi

and Ancona

, Distributed Runtime Verification of JADE Multiagent Systems, Vol. 570, 2015, 81–91.

Burigana

Fabiano

Dovier

and Pontelli

, Modelling multi-agent epistemic planning in ASP, Theory and Practice of Logic Programming 20(5) (2020), 593–608.

Cliffe

, Specifying and analyzing institutions in multi-agent systems using answer set programming, The Knowledge Engineering Review 24(4) (2009), 411.

10.

Coelho

Cirilo

Kulesza

Von Staa

Rashid

and Lucena

, JAT: A test automation framework for multi-agent systems, in: IEEE International Conference on Software Maintenance, ICSM, 2007, pp. 425–434.

11.

Douha

Mokhtari

and Guessoum

, Towards a non monotonic agent testing, reasoning about messages and behaviorï¼Œ in: 8th ACS/IEEE International Conference on Computer Systems and Applications AICCSA 2021, 2021.

12.

Enoiu

and Frasheri

, Test agents: Adaptive, autonomous and intelligent test cases, CoRR, abs/1802.03921, 2018.

13.

Febbraro

Leone

Reale

and Ricca

, Unit testing in ASPIDE, in: Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7773 LNAI, 2013, pp. 345–364.

14.

Fuxman

Liu

Mylopoulos

Pistore

Roveri

and Traverso

, Specifying and analyzing early requirements in Tropos, Requirements Engineering 9(2) (2004), 132–150.

15.

Gamma

, Design patterns: elements of reusable object-oriented software, Pearson Education India, 1995.

16.

Gelfond

and Lifschitz

, Classical negation in logic programs and disjunctive databases, New Generation Computing 9(3–4) (1991), 365–385.

17.

Giordano

Martelli

and Dupré

D.T.

, Verification with answer set programming, reasoning about actions and change, constraints and ontologies, in: CEUR Workshop Proceedings, Vol. 2509, 2020, pp. 41–46.

18.

Giordano

Martelli

Spiotta

and Dupŕe

D.T.

, ASP for reasoning about actions with an EL knowledge base, in: CEUR Workshop Proceedings, Vol. 1645, 2016, pp. 217–229.

19.

Lacey

and Deloach

, Verification of Agent Behavioral Models, in: The 2000 International Conference on Artificial Intelligence (IC-AI 2000), 2001.

20.

Lam

D.N.

and Barber

K.S.

, Verifying and explaining agent behavior in an implemented agent system, in: Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, 2004. AAMAS 2004, 2004, pp. 1226–1227.

21.

Laville

Lang

Herrmann

Philippe

Mazouzi

and Marilleau

, MCMAS: A toolkit for developing agent-based simulations on many-core architectures, Multiagent and Grid Systems 11 (2015), 15–31.

22.

Lifschitz

and Woo

T.Y.C.

, Answer Sets in General Nonmonotonic Reasoning (preliminary report), in: Proceedings of the Third International Conference on Principles of Knowledge Representation and Reasoning, 1991, pp. 603–614.

23.

Liu

Zhang

Dong

J.S.

Liu

Sun

Biswas

and Mokhtari

, Formal analysis of pervasive computing systems, in: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, IEEE, 2012, pp. 169–178.

24.

Menéndez

H.D.

Jahangirova

Sarro

Tonella

and Clark

, Diversifying focused testing for unit testing, ACM Transactions on Software Engineering and Methodology (TOSEM) 30(4) (2021), 1–24.

25.

Myers

, The Art of Software Testing, Second edition, Vol. 15, 2004.

26.

Nguyen

Perini

Tonella

and Kessler

, Automated continuous testing of multi-agent systems, In The fifth European Workshop on Multi-Agent Systems, 2007.

27.

Nguyen

C.D.

Miles

Perini

Tonella

Harman

and Luck

, Evolutionary testing of autonomous software agents, Autonomous Agents and Multi-Agent Systems 25(2) (2012), 260–283.

28.

Nguyen

C.D.

Perini

and Tonella

, ECAT: A tool for automating test cases generation and execution in testing multi-agent systems, in: Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol. 3, 2008, pp. 1623–1624.

29.

Opfer

Niemczyk

and Geihs

, Multi-agent plan verification with answer set programming, in: ACM International Conference Proceeding Series, 2016, pp. 32–39.

30.

Perini

Pistore

Roveri

and Susi

, Agent-oriented modeling by interleaving formal and informal specification, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2935 (2003), 36–52.

31.

Preuveneers

and Berbers

, Consistency in context-aware behavior: a model checking approach, in: Intelligent Environments (Workshops), 2012, pp. 401–412.

32.

Rakib

and Haque

H.M.U.

, A logic for context-aware non-monotonic reasoning agents, in: Mexican International Conference on Artificial Intelligence, Springer, 2014, pp. 453–471.

33.

Rakib

and Haque

H.M.U.

, Modeling and verifying context-aware non-monotonic reasoning agents, in: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), IEEE, 2015, pp. 61–69.

34.

Reiter

, A logic for default reasoning, Artificial Intelligence 13(1–2) (1980), 81–132.

35.

Roungroongsom

and Pradubsuwun

, Formal verification of JADE behaviour: A modeling approach, in: 2015 12th International Joint Conference on Computer Science and Software Engineering (JCSSE), 2015, pp. 180–183.

36.

Sama

Elbaum

Raimondi

Rosenblum

D.S.

and Wang

, Context-aware adaptive applications: Fault patterns and their automated identification, IEEE Transactions on Software Engineering 36(5) (2010), 644–661.

37.

Sartoli

and Namin

A.S.

, Modeling adaptive access control policies using answer set programming, Journal of Information Security and Applications 44 (2019), 49–63.

38.

Son

T.C.

Pontelli

Gelfond

and Balduccini

, Reasoning about truthfulness of agents using answer set programming, in: Proc. Int. Workshop Tempor. Represent. Reason., 2016, pp. 605–608.

39.

Sun

Liu

Dong

and Pang

, Towards flexible verification under fairness, in: CAV â€˜09: 21th International Conference on Computer Aided Verification, 2009, pp. 709–714.