Petri net and rewriting logic based formal analysis of multi-agent based safety-critical systems

Abstract

The formal design and development of multi-agent systems has attracted a considerable attention over the past decades because of their extensive use in safety-critical applications. This paper presents an efficient, hybrid and scalable formal development approach for safety-critical systems based on the multi-agent paradigm. In fact, we aim in this paper to benefit from the advantages of existing tools and techniques for each development stage and then integrate them in one unified approach. In particular approach, we advocate using Petri nets and rewriting logic to facilitate the formalization of multi-agent based systems, as well as we have integrated both the model checking and property-based testing techniques in the verification and testing stages. For illustrating the utilization and effectiveness of the proposed approach, we use it to analyze a simple automated distributing machine.

Keywords

Multi-agent system model-checking property-based testing petri net rewriting logic

1. Introduction

In the past few decades, the technological expansion in computer science and electronic domains have led to a variety of innovative software systems; later, so-called the revolution of electronic digital computer. Thereafter, software systems are becoming increasingly present in our environment for personal use, such as microwaves, mobile phones, washing machines, digital cameras, as well as for collective use, such as military, medical and aeronautics. In fact, these systems have not only facilitated to make our daily activities more comfortable, but it is becoming so clear that our lives are shaped and increasingly controlled by software systems to the extent that we cannot even imagine our world without them. However, such software systems are also responsible for an ever-increasing disastrous scenarios when it comes to safety-critical systems.

In this context, the use of multi-agent systems (MAS) has proven to be one of the most relevant approaches to promote the development of real-time [91, 47] and complex systems [31, 110]. Nevertheless, due to the absence of available agent-specific safety analysis methods, it is quite risky to completely trust agent-oriented methods in situations where safety is critical [12, 24]. Hence, the main interest in developing software for such systems is not just confined to clearly defining the system functions, interaction between components and properties of interest, but primordially on how one can identify and eliminate system errors in each development stage in order to ensure a successful implementation of the overall system.

To meet the high quality level and safety objectives satisfying the rising complexity of safety-critical systems, the use of adequate design approaches that support decentralized processing as well as rigorous analysis techniques and methods necessary to specify, design, implement and assess safety-related software systems, is gaining more and more importance.

1.1 Motivation

The present work is motivated by a desire to bridge the gap between formal specification, verification and testing during the design and development of multi-agent based critical systems. In this regard, the following issues must be addressed to increase the trustworthiness of safety-critical systems:

i.
The choice of the formalism for behavioral modeling of the safety-critical system.
ii.
The choice of a verification technique to ensure the correctness of the proposed model before proceeding to the system realization.
iii.
The choice of the code testing technique to ensure the absence of errors throughout the implementation stage.

In this context, Multi-Agent Systems (MAS) represent an innovative paradigm for modeling, simulating and designing complex distributed systems [101, 7]. Their effectiveness is due to the ability of agents to represent the system entities, their behaviors and interactions. In fact, an agent has proactive and reactive features that are very useful in decision making. In addition, a key characteristic of MAS is the collective intelligence or distributed intelligence. In this context, it is well known in the domain of MAS that a single ant or bee (agent) is not smart, but their colonies are generally characterized by numerous additional capabilities [87], such as solving complex tasks and finding the shortest path to the food source. Moreover, MAS can continue to function even with the failure of one of its components (agent), without degrading the system as a whole. This last feature is extremely important in the case of safety-critical systems. Therefore, the use of multi-agent systems is very advantageous for modeling safety-critical systems[2, 63, 71]. Nevertheless, given the lack of a formal, standardized method for the development of agent-based systems, software engineering for agent-based critical systems is quite challenging.

Petri nets [83] represent a well-defined theoretical model of concurrency in which the temporal ordering and causal relationships between system actions can be easily represented. Therefore, Petri nets are widely accepted for modeling and analyzing complex, dynamic and concurrent systems, like command and control systems [107], industrial real-time applications [41] and safety-critical systems [82, 90]. In addition and in the context of MAS, Petri nets are one of the most reliable formalisms for simulation and analysis of both behavioral modeling and failure analysis [44]. One of the distinguishing features of Petri nets is that they provide a graphical representation of the dynamic behavior of systems by enabling visualization of the state changes in the modeled system that greatly facilitates the analysis process [97]. These features of Petri nets are the key reason behind their wide popularity in the context of MAS [43, 54]. However, this potential of Petri nets should not deter the inherited difficulties and the increasing need for formal methods [89] and tools facilitating the analysis of large scale Petri net models.

For this purpose, we advocate the use of Maude [32] on the specification stage as a formal specification language based on rewriting logic [68] for describing Petri nets based MAS models. However, the existing rewriting logic based framework for Petri nets [94] needs some enhancements, namely, additional operators to facilitate counting or testing the number of tokens in a Petri net place. In addition, Petri nets require automatic tools to facilitate the transcription of their models into Maude specifications. This step is usually quite time consuming and error-prone in the case of large scale and complex models when performed manually. In order to overcome these limitations, we propose to benefit from this work [18], which presents an efficient algorithm allowing the automatic generation of Maude specifications for multi-agent system models based on Petri nets. Moreover, the choice of using Maude is also motivated by the availability of an integrated tool set that facilitates the formal verification of Petri net models, such as Maude model-checker [39], the reachability analysis tool and Maude’s inductive theorem prover (ITP) [52].

Similarly, we advocate the use of property-based testing (PBT) [75], which is an automatic verification technique of the proposed code skeletons based on random generation of test sequences (i.e. test scenarios). Contrary to the classic testing, the PBT technique is used to automatically test code skeletons or algorithms before implementation [56, 27].

The main objective of this work is on the formal analysis of MAS based safety-critical systems by the proposition of a new approach that covers almost all the development stages. To the best of our knowledge, both the enhanced Petri net specification and the combination of model checking with PBT techniques has never been used in a similar context before.

The remainder of this paper is structured as follows: Section 5 discusses some related works. Then, Section 2 presents an overview about MAS formalization. In Section 3, we briefly present our proposed approach for the formal analysis of multi-agent based safety-critical systems followed by a simple case study to show its feasibility in Section 4. Finally, Section 6 concludes the paper and presents some perspectives for future work.
2. Multi-agent based systems formalization: An overview

Formalization is a process that starts with the construction of a formal model (a precise description of the system structure, services and relationships) of the targeted system. Its purpose is to assist designers in proving the conformity of the system with its specification.

In this context, a large number of approaches, programming languages and graphical (or textual) formalisms have been used to describe all aspects of multi-agent systems such as CASL [15], SLABS [100], XABSL [86] and others [95, 9]. Nevertheless, it would be difficult to present an exhaustive list of all these works, and we therefore recall only a few works that we consider very important from the point of view of their relevance and their widespread usage.

2.1 Specification approaches

On the basis of specification formalisms and languages, one can easily find that Petri nets are still considered as one of the most used formalisms to help designers formalize and simulate MAS models [54, 80]. For instances, Petri nets and derivatives have been widely used to describe the social and behavioral aspects of agents [29, 88], interaction protocols [66] as well as cooperation and coordination in multi-agent systems [53]. Indeed, Petri nets have also been favored for the analysis of multi-agent systems because of the exact mathematical definition of their semantics of execution as well as the theory developed around them. The corresponding Petri net models of the multi-agent based systems are evaluated using the existing analysis methodologies and simulation techniques for Petri nets [30, 20].

Similarly, Maude has been used in several works for the formal specification of multi-agent systems [35, 3]. In addition, Maude was used to implement a (simplified language of) cognitive agent programming language 3APL in [99]. This work has been enhanced for prototyping the BUpL agent programming language (Belief Update programming language) and for executing agent programs [98]. Moreover, Maude is used in [61, 19] to formalize their agent based models, which are then simulated and verified using associated tools. However, the main disadvantage of all these works is that the translation of the models of the multi-agent systems to a Maude specification is done manually and in an ad hoc manner. It can therefore be quite difficult to ensure that this specification is a true description of the models of multi-agent systems studied especially in the case of complex models.

In this context, UML [10, 36] is widely used to describe the different aspects of multi-agent systems. In addition, the UML language has been a subject of several extensions to capture other aspects of multi-agent systems. For example, AML [28], MAS-ML [48] and AUML [96]. Moreover, many other works have emerged to develop a special Object Constraint Language (OCL) [79, 73] allowing to reduce the ambiguity and the misunderstanding of the models by specifying additional constraints on the behavior of the components of the studied system.

Similarly, architecture description languages (ADLs) are a particular type of languages that provide a concrete syntax for specifying system architectures in a more abstract, flexible and robust way than other traditional approaches. They have been widely used for the description of architectures of multi-agent systems [50, 33].

Except some works that propose a formal UML (or ADL) based description for MAS [70, 21], the major problem with most ADLs and UML is that they lack formal semantics, explicit support for running a description of the architecture, and ensuring compliance between a system and a user-specified architecture. For instance, some works were focused on the translation or combination of UML [42, 40] and ADLs [85, 84] into Petri nets to benefit from the existing formal analysis tools. Other authors attempted to translate UML diagrams [6, 69] and software architecture description language models [104, 74] into rewriting logic. Moreover, some authors proposed rewriting logic (resp, Petri net) based ADLs [46, 92] (resp, [106, 57]) in order to obtain a formal description and simulation mechanism for the studied system architecture.

2.2 Verification approaches

The verification of multi-agent systems is gaining more importance [72, 60]. For instance, a considerable amount of work has been done to verify the behavior of agents [93, 105], analyzing interaction protocols and their communication languages [67, 4] as well as to simulate and control security in multi-agent systems [22, 109]. However, we can see that the existing research works are generally directed towards the creation of verification tools for multi-agent systems, otherwise, they are based on existing model checkers. Table 1 presents a summary of the most known model-checkers based works, alongside the used formalism for system and/or property specification.

Table 1
Summary of works using model-checkers for MAS verification

Work	System specification	Property specification	Verification tool	Year
Wooldridge et al. [103]	MABLE	LORA	SPIN	2002
Benerecetti et al. [14]	Binary Decision Diagrams	MATL	NuMAS	2002
Bordini et al. [16, 17]	AgentSpeak(F)	LTL	SPIN	2003
Gammie et al. [45]	Binary Decision Diagrams	CTL/LTL	MCK	2004
Lomuscio et al. [65]	Interpreted systems programm-ing language (ISPL)	Alternating-time
Temporal Logic (ATL)	MCMAS	2006
Belala et al. [11]	Multi-Formalisms	LTL	Maude model-checker	2006
Riemsdijk et al. [99]	3APL	LTL	Maude model-checker	2006
Lomuscio et al. [64]	Interpreted Systems	CTLK	NuSMV	2007
Rodion et al. [78]	Alloy	Alloy’s relational algebra	Alloy Analyzer	2007
Boudiaf et al. [19]	Rewriting Theories	LTL	Maude model-checker	2008
Nabialek et al. [58]	Multi-Formalisms	CTLKD	VerICS	2008
Astefanoaei et al. [8]	Normative MAS language	LTL	Maude Model-Checker	2009
D’Souza et al. [37]	State Chart Diagrams	CTL	NuSMV2	2012
Laouadi et al. [61]	Agent UML	LTL	Maude Model-Checker	2017
Jeremy et al. [59]	Interpreted Systems	CTLK	MCMAS	2017

2.3 Synthesis

The specification of a multi-agent system involves the identification of a large number of entities and their relationships. For this, several types of formalisms have been used to construct the most appropriate system model to verify the properties in question and not to be limited – if necessary – on the use of a single formalism so to manage the different perspectives of the system [81].

In this context, we can easily deduce that Petri nets and rewriting logic are quite well-suited for MAS modeling and specification. At the verification stage, Maude is widely used as a formal semantic framework in many works for the verification of multi-agent systems and therefore its use is very appropriate and endorsed.

In addition, within the scope of enhancing multi-agent based systems quality, numerous other testing based works have been realized [13, 26]. However, it is better if testing strategies are combined (used jointly) with model checking based ones in order to better guarantee the system implementation quality.

Based on the literature review about MAS formalization, the fundamental steps of a formal analysis approach of multi-agent based systems can be summarized in the following three points:

i.
Clearly define the structure and behavior of the system using the appropriate modeling formalisms and/or the most adapted formal specification languages.
ii.
Identify the risks and errors of the system – which may be catastrophic or expensive – to support and better verify its corresponding properties using formal verification techniques.
iii.
Ensure that the system implementation meets the specification and that the proposed code will not make errors using advanced testing techniques.

3. Proposed formal analysis approach of multi-agent based safety-critical systems

The proposed approach for the formal development and analysis of behavioral aspect of multi-agent based safety-critical systems contemplates the following phases of software development: modeling, specification, validation, and testing. The next subsections provide an overview of each stage of the proposed approach.

3.1 Modeling stage

The goal of this first stage is to construct the Petri net model formalizing the dynamic behavior of the studied system. In addition, the designer uses rewriting logic, which is a very expressive logic to give formal semantics when specifying Petri net models. Depending on the system studied, a system may have several operational phases, generally: startup, initialization, processing etc. Usually, each operational phase may have its own model. Therefore, it is necessary in the case of some complex systems to built more than one model, and according to the property or aspect to be verified, the designer must prepare an independent (separate) Petri net model before the complete model is developed.

3.2 Specification stage

This stage is intended to prepare two specification levels:

a)
System specification: The main objective of the specification level is to translate the proposed model into rewriting logic by using an enhanced proposed specification for Petri nets based on rewriting logic.
b)
Properties specification: If the aim of system specification level, is to give a more or less abstract description of the system then the system can be formally defined by its properties. In this step, we refer to the created model and its specification to prepare a module that defines the set of predicates expressed in standard LTL propositional logic. These predicates are considered by the Maude’s model-checker tool as the set of verified properties in the system. Then, the set of properties to be checked must be expressed in LTL as well.

3.3 Verification stage

The verification stage is used to show that the system satisfies the desired properties and that it exhibits a stable behavior, and/or certifies that the probable malfunctions of the system will not causes damages.

The following two verification tools may be used in this stage:

(a)
LTL model-checker: It checks the properties of a model by expressing them in linear temporal logic (LTL).
(b)
Search tool: This tool may overcome some of the shortcomings of the model-checking technique. For instance, it allows designers to check the absence/existence of some worst-cases – offered by experts in the field – that may not be expressible in LTL. In addition, it presents all the possible scenarios for the such worst-cases if they exist, which is not the case for the model-checker counter example (single scenario).

3.4 Testing phase

The more complex a software system is, the more difficult (or unfeasible) its formal verification becomes. In addition, even if the model has been completely verified by model checking techniques, its full realization also needs to be tested. In the final stage of our approach, we advocate to use property-based testing to test the proposed implementation of the SUT. Therefore, we define all desired properties in addition to those that have not been verified in earlier phases as universally quantified expressions, and devote as much time as available to automatically generate, run, and evaluate them as test cases. In this step, we propose to use QuickCheck’s capabilities to produce shunk (i.e. simplified) counterexamples when a specific test case is found to show how that the realization of the system violates a given property.

Table 2
Meaning of Petri net places and transitions

Place labels with meaning
P1	A visitor is coming and waiting for the machine to start up
P2	Machine in the state Idle (sleep)
P3	A visitor is ready (to insert his card)
P4	Machine is ready for use
P5	A visitor is using the machine (waiting test and/or services)
P6	Card is inserted
P7	Card is tested
P8	Invalid card is rejected
P9	Delivering service 1 and rejecting card
P10	Delivering service 2 and rejecting card
Transition labels with meaning
T1	Add new visitor to use the machine
	(only if there is no one waiting, ready or using the machine)
T2	A visitor pushes the start button of the machine
T3	Changing visitor state to ready
	(if the machine is not in the sleep state)
T4	The machine returns to the Idle state
	(if there is no visitor in ready state)
T5	Inserting card
T6	Testing card
T7	Rejecting invalid card
T8	Visitor takes invalid card and goes away
T9	Accepting card and delivering service 1
T10	Visitor takes his card with service 1 and goes away
T11	Accepting card and delivering service 2
T12	Visitor takes his card with service 2 and goes away

Figure 1.

Petri Net model of the automatic distributor.

4. Case study

4.1 System description and modeling

To show the practical usefulness and effectiveness of the proposed approach, we consider a simple automated distributing machine placed in a hotel to provide coffee, cakes and beverage items to hotel visitors. The visitor has to use his magnetic hotel visitor card to gain services from the machine.

Such a machine is daily programmed to deliver a cup of coffee, cake with a bottle of water and juice (Service 1) to the visitor upon the first usage of his card. Otherwise, the machine delivers only coffee and cake (Service 2). For that, the machine tests the inserted card to check its validity and determines if it is the first use for a card or no. Thereafter, the corresponding service is delivered.

For the sake of simplicity, we assume that the visitor card contains a bar code with 14 digits where the addition of digits in positions (1, 2, 4, 8) equals to 20. In addition, the card codes of the present visitors in the hotels are inserted daily in a list into the memory of the machine and when a valid visitor card is used, it will be automatically deleted from this list. Such a mechanism facilitates the process to deliver Service 1 or Service 2 to a visitor.

Therefore, in both cases (Testing card validity and Determining services), two algorithms are used for verification. Figure 1 shows the Petri net that models the described machine, and Table 2 presents the meaning of places and transitions.

4.2 System and properties specification

We should note that the existing rewriting logic semantics for Petri nets does not support (without other additional operators) neither the specification of inhibitor arcs nor counting the number of tokens in a specific place. Therefore, we propose an enhanced specification that alleviates such two limitations.

4.2.1 System specification

The corresponding rewrite theory of the Petri net model is illustrated in Snippet 1. In this specification, the static aspect (the signature) of the system is defined in the functional module PETRI_NET. This module has been imported in the system module PN_ADM, in which we add a rule for each transition to complete describing the dynamic aspect of the machine.

Snippet 1: Petri net Maude specification.

4.2.2 Properties specification

In the case of our system, the following properties have to be verified:

a)
System evolution: This property ensures that the system is always (or able to be) active and it will not be blocked in a deadlock situation.
b)
Serving visitors: This property ensures that whenever a visitor is present and wants to take something from the machine, he must be served, either by Service 1, Service 2 or his card is rejected if it is not valid.
c)
Determining services: This property ensures that each visitor gets Service 1 at the first time and Service 2 after that. In fact, this property is very important for the hotel due to the financial loss it can incur. Therefore, it must be rigorously verified.

Then, two modules for the specification of system properties are prepared. The first module, PN_ADM_PREDS, describes of the set of properties that are assumed to be verified in the model and that will be used as a reference in the process of verification by the model checking tool. However, in the second module, ACS-CHECK, the designer expresses the relevant properties to be checked in the system model. This module contains the properties that are expressible in LTL only. These modules are illustrated in the following Snippet 2:

Snippet 2: System properties specification in Maude.

4.3 Verification

Starting from the initial state of the Petri net, the Maude LTL model-checker has been used for the verification of two properties.

a)
System evolution: This property is defined in the module ADM-CHECK as “no-deadlock”. Figure 2 shows the execution result confirming the correctness of this property.

Figure 2.
Model-checking the deadlock absence property.

b)
Serving visitors: This property is defined as “serving” in the module ADM-CHECK. The LTL model-checker also confirmed the correctness of this property (see Fig. 3).

Figure 3.
Model-checking the serving property.

4.4 Testing

As per the proposed approach, we used PBT to test the “Determining service" property mentioned in Section 4.2.2. In fact, this property is not expressible as a LTL formula and cannot be verified even by the Maude “search tool” since it is related to the implementation and not to the system model. However, it can be translated into a number of declarative properties, such as given in Snippet 3:

Snippet 3: Erlang code for the positive testing of the third property.

These two functions aim to test the two possibilities when it comes to the service control: either the client should get the first service when using the machine, or else the card had already been used and so the service should be the second type. These statements should hold for all the valid client cards that we test.

In this first formulation, the kind of testing to be performed is positive testing, since only valid client cards are generated to be used as input. The valid_client_card function is a data generator that, to comply with the description in Section 4.1, could be implemented as given in the following Snippet 4:

Snippet 4: Erlang code for the data generator.

where nat() is a QuickCheck data generator that produces random natural numbers. Our customized generator produces sequences of 14 natural numbers, but only returns those that fulfill the condition P1+P2+P4+P8 == 20.

The additional helper functions proper_first_service and proper_second_service are used to check the result of invoking the functionality under test on the SUT (sut:use_machine (Client)). We include them here to illustrate how using the Erlang version of QuickCheck allows us to implement these kinds of test codes, regardless of the actual technology used to implement the SUT. In fact, the properties needed to be defined in a declarative manner, using the typical artefacts of a functional language (such as pattern-matching, heavily exploited here), like Erlang as given in the Snippet 5:

Snippet 5: Erlang code for additional helper functions.

Finally, we take advantage of recursion to implement one last helper to invoke the SUT a random number of times, to simulate the card being used $n$ times after the first time (see Snippet 6). Again, for all $n$ s that we generate, the above property should hold.

Snippet 6: Erlang code for simulating the random number of execution.

Running these properties as many times as desired will increase our confidence in the SUT implementation if we are unable to find a counterexample (1000 tests for instance, see Fig. 4). Of course, this is not as strong as proving that the SUT is correct, but it is the best that can be done using testing.

Figure 4.

PBT of the determining service property.

Of course, we could also formulate the previous two properties to perform negative testing as well, i.e. generate valid and invalid inputs, and state that only if the input is valid, the property is expected to hold. These new properties could be defined as shown in Snippet 7.

Snippet 7: Erlang code for the negative testing of the third property.

where the new data generator any_client_card will now only produce sequences of 14 natural numbers, and another helper function, valid_client_card would be used for determining whether the body of the function is expected to be true or not (see Snippet 8):

Snippet 8: Erlang code for testing valid cards.

If the SUT had a similar functionality to that of valid_client_card then it should be tested against this helper function in a property that states that for all client cards, both the helper function and the SUT implementation should generate the same output for a given card.

Last but not least, we could also test the behaviour of the SUT when a card is invalid. In doing so, we would generate invalid card data on purpose, and test that invoking the SUT always returns the no service message. This property can be expressed as shown in Snippet 9:

Snippet 9: Erlang code for testing invalid cards.

4.5 Discussion and motivation

Based on the above-mentioned analysis, we now highlight the main advantages of the proposed approach. In the modeling stage, we justify the selection of the Petri net among many other formalisms, such as UML diagrams, and architecture description languages (ADL) based on the following points:

i)
Expressiveness: In addition to the intuitive graphical representation, the expressiveness of Petri nets, makes it a very suitable formalism for modeling and analyzing a rich variety of systems and applications including, concurrent, distributed and critical system architectures.
ii)
Formal Semantics: Since Petri Net is one of the most important formalisms having a well-defined formal semantic and theoretical foundation, it is widely used to formalize not only systems but even other modeling techniques and description languages that are used to describe software architecture (see, Subsection 2.1).
iii)
Formal analysis: Petri net has gained wide acceptance as a modeling technique in both industrial and academic areas because of the existence of a large number of analysis tools [102, 51] and techniques [55] for Petri net based models.

The specification language used in our approach is Maude. This choice is motivated by the expressiveness, modularity and parametrization of Maude. Moreover, the rewriting logic allows us to naturally express both flat and hierarchically composite Petri net models. Finally, the availability of a large number of integrated tools, such as Maude model-checker [39] and Maude search tool, facilitate the formal verification of Petri net models in the verification stage. These tools cannot be used to analyze infinite-state systems, and for such systems Maude supports reachability analysis and model checking, including model checking for a useful class of temporal logic formulas. Furthermore, due to the reflective nature of its logic and its implementation, such a library can be easily extended by the user with new model checking strategies.

Because of the excellent results obtained in the context of MAS [13], we advocate the use of property-based testing (PBT) for the testing stage. Indeed, testing is the last checkpoint at which software errors can be detected before a system goes into operation. However, it leaves all responsibility of designing and writing test scenarios to a human developer, who is limited by time constraints and usually based on his/her own experience and views on the SUT [108]. PBT has proven to play a vital role – as an automatic technique – in detecting corner cases that usually slip through human-conducted testing [34]. Moreover, PBT supports randomness for the generation of test sequences (i.e. test scenarios) themselves not only to alleviate the human factor, but also to compromise effort and correctness [49].

Consequently, we can say that we have proposed a generic approach that covers all software development stages. Thus, we have used rewriting logic as a unifying semantic framework in the specification stage, Maude model checking tool to check model properties, and finally QuickCheck’s property-based testing at the implementation level, to raise the confidence on the realization of the given system.
5. Related work

Safety-critical systems refer to systems in which failures may lead to catastrophic consequences, such as loss of human life, significant damage to the environment, and/or financial disasters. Multi-agent systems have been widely used to develop [23, 38], simulate [1], secure [77] and analyze [62] critical systems.

A formal methodology was proposed in [2] to ensure the correctness properties of safety and liveness of the Mail Transport System. While specifying Gaia based multi-agent requirement and design specifications, authors used regular expression in specifying the liveness properties and the first-order predicate calculus to specify the safety properties. In the verification stage, The Finite State Processes (FSP) and Labelled Transition System (LTS) are used. Then, Event-B is utilized for an exhaustive analysis.

Similarly, a multi-agent approach is proposed in [71] to ensure the reliability problem of an Air Traffic Control (ATC). Therefore, an agent-based decision-aided system was developed to help controllers in using their multiple software tools in critical situations such as the unavailability of some tools due to technical incidents. Practically, a simulation environment is used to test the MAS and demonstrate its significance to air traffic controllers.

A simulation-based hazard analysis method using multi-agent modeling has been presented in [5] to explore the effects of deviant node behaviour within a System of System (SoS). In comparison with traditional hazard analysis techniques, the presented method has demonstrated its effectiveness in revealing hidden and undiscovered hazards.

In addition, a formal development of a hospital MAS by refinement in Event-B has been presented in [76]. In this work, authors focused on modeling and verifying some safety critical activities, such as consistent updates of patient data and handling emergencies. The main properties of MAS have been formalized and demonstrated using Event-B. However, due to the autonomous agent behaviour, the highly dynamic nature of a hospital and volatile error-prone communication environment, ensuring correctness of these activities was not a trivial task.

Moreover, in [25], agent-based modeling has been investigated to study and simulate the interdependencies in critical infrastructures. In fact, authors had proposed to adopt UML for better representing the interdependencies between the different components of the critical system. Thereafter, it has been exploited to simulate such complex systems through multi-agent paradigm.

Analyzing the characteristics of the presented works, we can conclude that a promising approach for developing multi-agent based safety-critical system can be very advantageous if it based on Petri nets as a well-defined theoretical model of concurrency on the modeling stage. Then, the use of rewriting logic at the specification stage can provide many benefits for both specification and verification purposes because of the formal analysis tools associated with Maude. Finally, the integration of a powerful technique to ensure the absence of code error during the system implementation can faciltate the usage of such an approach in critical system context.

6. Conclusion and future work

In this paper, we have presented a new user-friendly approach for the formal analysis of behavioral software architecture of multi-agent based safety-critical systems. The proposed approach has been tested on a case study and results have been found to be quite promising. The ultimate objectives of our approach were:

Using the Petri net formalism in the modeling stage to prepare an appropriate model of the given system architecture. Then, the rewriting logic is used for the specification of petri net in an enhanced version that naturally allows the specification of inhibitor arcs and count tokens in a Petri net place.

Combining model-checking and PBT techniques to ensure the absence of any error or unexpected behavior in the specification and implementation of the software under design.

In the future, we plan to implement an algorithm for the automatic generation Petri nets specification based on the enhanced semantics. Such algorithm will enlarge and facilitate the use of our approach and permit developers to benefits from the Maude associated formal analysis tools while developing their safety-critical systems.

Footnotes

Authors’ Bios

	Ammar Boucherit is an associate professor at the University of El-Oued, Algeria. He holds his PhD degree in Computer Science from University of Ferhat Abbas, Sétif, Algeria. His research focused on three areas: formal design of computer systems, software architecture and multi-agents systems.
	Laura M. Castro is an associate professor at the University of A Coruña, Spain. She is a member of the MADS (Models and Applications of Distributed Systems) research group. Her research focuses on software testing (automated, model and property-based testing), applied to software in general, and distributed, concurrent, functional systems in particular.

Abdallah Khababa is currently a full professor at the University of Ferhat abbas Sétif, Algeria. He holds a Ph.D. in computer science from the University of Ferhat Abbas Sétif. His main areas of interest includes cognitive science and artificial intelligence, knowledge representation with ontologies and human-machine interface and its usability.

Osman Hasan is the senior head of department of electrical engineering SEECS and the director of the system analysis and verification (SAVe) Lab at NUST SEECS. Prior to joining NUST SEECS, He did his PhD and post-doctoral fellowship from the hardware verification group at Concordia University, Montreal Canada. His main research interests include formal verification, interactive theorem proving and higher-order logic.

References

Aguilar

Lalith

and Hori

, Time critical mass evacuation simulation combining a multi-agent system and high-performance computing, Multi-agent Systems, 2017, p. 17.

Akhtar

and Hussain

, Formal modeling of a mail transport system based on multi-agent system-of-systems, Journal of Information Communication Technologies and Robotic Applications, 2019, pp. 68–79.

Akhtar

and Missen

M.M.S.

, Contribution to the formal specification and verification of a multi-agent robotic system, arXiv preprint arXiv:1604.05577, 2015.

Alberti

Daolio

Torroni

Gavanelli

Lamma

and Mello

, Specification and verification of agent interaction protocols in a logic-based system, In Proceedings of the 2004 ACM symposium on Applied computing, ACM, 2004, pp. 72–78.

Alexander

and Kelly

, Supporting systems of systems hazard analysis using multi-agent simulation, Safety Science 51(1) (2013), 302–318.

Aoumeur

and Saake

, Integrating and rapid-prototyping uml structural and behavioural diagrams using rewriting logic, In CAiSE, Springer, 2002, pp. 296–310.

Arki

Zitouni

Dib

and Taki

, A multi-agent security framework for cloud data storage, Multiagent and Grid Systems 14(4) (2018), 357–382.

Astefanoaei

Dastani

Meyer

J.-J.C.

and de Boer

F.S.

, On the semantics and verification of normative multi-agent systems, J UCS 15(13) (2009), 2629–2652.

Barwell

A.D.

Brown

Hammond

Turek

and Byrski

, Using program shaping and algorithmic skeletons to parallelise an evolutionary multi-agent system in erlang, Computing and Informatics 35(4) (2017), 792–818.

10.

Bauer

and Odell

, Uml 2.0 and agents: how to build agent-based systems with the new uml standard, Engineering Applications of Artificial Intelligence 18(2) (2005), 141–157.

11.

Belala

and Boucherit

, A contribution to the formal checking of multi-agents systems, In IEEE International Conference on Computer Systems and Applications, 2006, IEEE, 2006, pp. 9–16.

12.

Benabdellah

A.C.

Bouhaddou

and Benghabrit

, Supply chain challenges with complex adaptive system perspective, In World Conference on Information Systems and Technologies Springer, 2018, pp. 1081–1093.

13.

Benac Earle

and Fredlund

L.-Å.

, A property-based testing framework for multi-agent systems, In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, IFAAMAS, 2019, pp. 1823–1825.

14.

Benerecetti

and Cimatti

, Symbolic model checking for multi-agent systems, Proc. MoChart 2 (2002), 1–8.

15.

Birdsey

Szabo

and Falkner

, Casl: a declarative domain specific language for modeling complex adaptive systems, In Proceedings of the 2016 Winter Simulation Conference, IEEE Press, 2016, pp. 1241–1252.

16.

Bordini

R.H.

Fisher

Pardavila

Visser

and Wooldridge

, Model checking multi-agent programs with casp, In International Conference on Computer Aided Verification, Springer, 2003, pp. 110–113.

17.

Bordini

R.H.

Fisher

Pardavila

and Wooldridge

, Model checking agentspeak, In Proceedings of the second international joint conference on Autonomous agents and multiagent systems, ACM, 2003, pp. 409–416.

18.

Boucherit

Khababa

and Castro

L.M.

, Automatic generating algorithm of rewriting logic specification for multi-agent system models based on petri nets, Multiagent and Grid Systems 14(4) (2018), 403–418.

19.

Boudiaf

Mokhati

and Badri

, Supporting formal verification of dima multi-agents models: towards a framework based on maude model checking, International Journal of Software Engineering and Knowledge Engineering 18(7) (2008), 853–875.

20.

Brahimi

Maamri

and Sahnoun

, Dynamic verification of hierarchical multi-agent plans, Multiagent and Grid Systems 13(2) (2017), 113–142.

21.

Broy

and Cengarle

M.V.

, Uml formal semantics: lessons learned, Software and Systems Modeling 10(4) (2011), 441–446.

22.

Bulut

Khadraoui

and Marquet

, Multi-agent based security assurance monitoring system for telecommunication infrastructures, In Proceedings of the Fourth IASTED International Conference on Communication, Network and Information Security, ACTA Press, 2007, pp. 90–95.

23.

Calvaresi

Albanese

Marinoni

Dubosson

Sernani

Dragoni

A.F.

and Schumacher

, Timing reliability for local schedulers in multi-agent systems, In RTcMAS@ IJCAI, 2018, pp. 1–15.

24.

Calvaresi

Marinoni

Sturm

Schumacher

and Buttazzo

, The challenge of real-time multi-agent systems for enabling iot and cps, In Proceedings of the international conference on web intelligence, ACM, 2017, pp. 356–364.

25.

Cardellini

Casalicchio

and Galli

, Agent-based modeling of interdependencies in critical infrastructures through uml, In Proceedings of the 2007 spring simulation multiconference-Volume 2, Society for Computer Simulation International, 2007, pp. 119–126.

26.

Carrera

Á.

Iglesias

C.A.

and Garijo

, Beast methodology: An agile testing methodology for multi-agent systems based on behaviour driven development, Information Systems Frontiers 16(2) (2014), 169–182.

27.

Castro

L.M.

Lamela

and Thompson

, Making property-based testing easier to read for humans, Computing and Informatics 35(4) (2017), 890–913.

28.

Cervenka

and Trencansky

, The Agent Modeling Language-AML: A Comprehensive Approach to Modeling Multi-Agent Systems, Springer Science & Business Media, 2007.

29.

Chatterjee

R.K.

Neha

and Sarkar

, Behavioral modeling of multi agent system: high level petri net based approach, International Journal of Agent Technologies and Systems (IJATS) 7(1) (2015), 55–78.

30.

Chatterjee

R.K.

Sarkar

and Bhattacharya

, Modeling and analysis of agent oriented system: Petri net based approach, In Proceedings of the International Conference on Software Engineering Research and Practice (SERP’11), 2011, pp. 17–23.

31.

Chennoufi

Bendella

and Bouzid

, Multi-agent simulation collision avoidance of complex system: application to evacuation crowd behavior, International Journal of Ambient Computing and Intelligence (IJACI) 9(1) (2018), 43–59.

32.

Clavel

Durán

Eker

Escobar

Lincoln

Martí-Oliet

and Talcott

, Two decades of maude, In Logic, Rewriting, and Concurrency, Springer, 2015, pp. 232–254.

33.

Darragi

El-Koursi

and Collart-Dutilleul

, Architecture description language for cyber physical systems analysis: a railway control system case study, Computers in Railways XIV: Railway Engineering Design and Optimization 135 (2014), 227–237.

34.

Derrick

Walkinshaw

Arts

Benac Earle

Cesarini

Fredlund

L.-A.

Gulias

Hughes

and Thompson

, Property-based testing – the protest project, LNCS 6286 LNCS: 250–271, 2010.

35.

Dib

A.T.

and Sahnoun

, Formal specification of multi-agent system architecture, In ICAASE, 2014, pp. 65–72.

36.

Dillon

D.S.

Dillon

T.S.

and Chang

, Using uml 2.1 to model multi-agent systems, In Software Technologies for Embedded and Ubiquitous Systems, Springer, 2008, pp. 1–8.

37.

D’Souza

Rao

Sharma

and Singh

, Modeling and verification of a multi-agent argumentation system using nusmv, arXiv preprint arXiv:1209.4330, 2012.

38.

Ehikioya

S.A.

and Zhang

, Real-time multi-agents architecture for e-commerce servers, International Journal of Networked and Distributed Computing 6(2) (2018), 88–98.

39.

Eker

Meseguer

and Sridharanarayanan

, The maude ltl model checker, Electronic Notes in Theoretical Computer Science 71 (2004), 162–187.

40.

Emadi

and Shams

, Transformation of usecase and sequence diagrams to petri nets, In Computing, Communication, Control, and Management, 2009. CCCM 2009. ISECS International Colloquium on, volume 4, IEEE, 2009, pp. 399–403.

41.

Fantechi

and Pepi

, Petri nets modeling for the schedulability analysis of industrial real time systems, In AMARETTO@ MODELSWARD, 2016, pp. 5–13.

42.

Fernandes

J.M.

, Combining petri nets and uml for model-based software engineering, CEUR Workshop Proceedings, 2012.

43.

Figat

and Zieliński

, Methodology of designing multi-agent robot control systems utilising hierarchical petri nets, arXiv preprint arXiv:1906.11614, 2019.

44.

Frasheri

Trinh

L.A.

Cürüklü

and Ekström

, Failure analysis for adaptive autonomous agents using petri nets, In 2017 Federated Conference on Computer Science and Information Systems (FedCSIS), IEEE, 2017, pp. 293–297.

45.

Gammie

and Van Der Meyden

, Mck: Model checking the logic of knowledge, In International Conference on Computer Aided Verification, Springer, 2004, pp. 479–483.

46.

Garlan

Schmerl

B.R.

and Cheng

S.-W.

, Software architecture-based self-adaptation, Autonomic Computing and Networking 1 (2009), 31–55.

47.

Glaschenko

Ivaschenko

Rzevski

and Skobelev

, Multi-agent real time scheduling system for taxi companies, In 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2009), Budapest, Hungary, 2009, pp. 29–36.

48.

Gonçalves

E.J.T.

Cortes

M.I.

Campos

G.A.L.

Lopes

Y.S.

Freire

E.S.

da Silva

V.T.

de Oliveira

K.S.F.

and de Oliveira

M.A.

, Mas-ml 2.0: Supporting the modelling of multi-agent systems with different agent architectures, Journal of Systems and Software 108 (2015), 77–109.

49.

Groce

Holzmann

and Joshi

, Randomized differential testing as a prelude to formal verification, In 29th International Conference on Software Engineering (ICSE’07), IEEE, 2007, pp. 621–631.

50.

Guan

, Prevention and control model of enterprise business risk based on multi-agent, Journal of Convergence Information Technology 5(7) (2010), 148–154.

51.

Heiner

Schwarick

and Wegener

J.-T.

, Charlie–an extensible petri net analysis tool, In International Conference on Applications and Theory of Petri Nets and Concurrency, Springer, 2015, pp. 200–211.

52.

Hendrix

Meseguer

and Sasse

, Maude itp 2.0 tutorial, Technical report, Technical report, University of Illinois at Urbana-Champaign, 2008.

53.

Hsieh

F.-S.

, Developing cooperation mechanism for multi-agent systems with petri nets, Engineering Applications of Artificial Intelligence 22(4–5) (2009), 616–627.

54.

Hsieh

F.-S.

, A hybrid and scalable multi-agent approach for patient scheduling based on petri net models, Applied Intelligence 47(4) (2017), 1068–1086.

55.

Huang

Y.-S.

Chung

T.-H.

and Su

P.-J.

, Synthesis of deadlock prevention policy using petri nets reachability graph technique, Asian Journal of Control 12(3) (2010), 336–346.

56.

Hughes

Norell

Smallbone

and Arts

, Find more bugs with quickcheck! In Proceedings of the 11th International Workshop on Automation of Software Test, ACM, 2016, pp. 71–77.

57.

Junior

M.N.

Maciel

Lima

Ribeiro

Oliveira

Arcoverde

Barreto

Tavares

and Amorin

, A retargetable environment for power-aware code evaluation: An approach based on coloured petri net, LNCS 3728 2005, 49.

58.

Kacprzak

Nabiałek

Niewiadomski

Penczek

Półrola

Szreter

Woźna

and Zbrzezny

, Verics 2007-a model checker for knowledge and real-time, Fundamenta Informaticae 85(1–4) (2008), 313–328.

59.

Kong

and Lomuscio

, Symbolic model checking multi-agent systems against ctl* k specifications, In Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, IFAAMAS, 2017, pp. 114–122.

60.

Kouvaros

and Lomuscio

, Automatic verification of parameterised multi-agent systems, In Proceedings of the 2013 international conference on Autonomous agents and multi-agent systems, IFAAMAS, 2013, pp. 861–868.

61.

Laouadi

M.A.

Mokhati

and Seridi-Bouchelaghem

, A formal framework for organization-centered multi-agent system specification: A rewriting logic based approach, Multiagent and Grid Systems 13(4) (2017), 395–419.

62.

Liu

C.L.

Kazmierczak

and Miller

, A safety analysis method for multi-agent systems, International Journal of Computer and Information Engineering 9(10) (2017), 2310–2319.

63.

Liu

Chen

Sun

and Hu

, Multi agent system based process control in wide area protection against cascading events, In 2013 IEEE Grenoble Conference, IEEE, 2013, pp. 1–6.

64.

Lomuscio

Pecheur

and Raimondi

, Automatic verification of knowledge and time with nusmv, In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, IJCAI/AAAI Press, 2007, pp. 1384–1389.

65.

Lomuscio

and Raimondi

, Mcmas: A model checker for multi-agent systems, In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2006, pp. 450–454.

66.

Marzougui

and Barkaoui

, Interaction protocols in multi-agent systems based on agent petri nets model, Int J Adv Comput Sci Appl 4(7) (2013).

67.

Mazouzi

Seghrouchni

A.E.F.

and Haddad

, Open protocol design for complex interactions in multi-agent systems, In Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, ACM, 2002, pp. 517–526.

68.

Meseguer

, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science 96(1) (1992), 73–155.

69.

Mokhati

and Badri

, Generating maude specifications from uml use case diagrams, Journal of Object Technology 8(2) (2009), 319–136.

70.

Mouratidis

Kolp

Giorgini

and Faulkner

, An architectural description language for secure multi-agent systems, Web Intelligence and Agent Systems: An International Journal 8(1) (2010), 99–122.

71.

Nguyen-Duc

Guessoum

Marin

Perrot

J.-F.

and Briot

J.-P.

, A multi-agent approach to reliable air traffic control, na, 2008.

72.

Niazi

M.A.

Hussain

and Kolberg

, Verification & validation of agent based simulations using the vomas (virtual overlay multi-agent system) approach, arXiv preprint arXiv:1708.02361, 2017.

73.

Ocl

, 2.0 specification, Final Adopted Specification ptc/03-10, 14, 2005.

74.

Ölveczky

P.C.

Boronat

and Meseguer

, Formal semantics and analysis of behavioral aadl models in real-time maude, In Formal Techniques for Distributed Systems, Springer, 2010, pp. 47–62.

75.

Paraskevopoulou

Hriţcu

Dénès

Lampropoulos

and Pierce

B.C.

, Foundational property-based testing, In International Conference on Interactive Theorem Proving, Springer, 2015, pp. 325–343.

76.

Pereverzeva

Troubitsyna

and Laibinis

, Formal development of critical multi-agent systems: A refinement approach, In 2012 Ninth European Dependable Computing Conference, IEEE, 2012, pp. 156–161.

77.

Pipattanasomporn

Feroze

and Rahman

, Securing critical loads in a pv-based microgrid with a multi-agent system, Renewable Energy 39(1) (2012), 166–174.

78.

Podorozhny

Khurshid

Perry

and Zhang

, Verification of multi-agent negotiations using the alloy analyzer, In International Conference on Integrated Formal Methods, Springer, 2007, pp. 501–517.

79.

Przigoda

Hilken

Wille

Peleska

and Drechsler

, Checking concurrent behavior in uml/ocl models, In 2015 ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MODELS), IEEE, 2015, pp. 176–185.

80.

Pujari

and Mukhopadhyay

, Petri net: A tool for modeling and analyze multi-agent oriented systems, International Journal of Intelligent Systems and Applications 4(10) (2012), 103.

81.

Ramat

, Introduction à la modélisation et à la simulation à événements discrets, Modélisation et simulation multi-agents: Applications pour les sciences de I’homme et de la société, 2006, pp. 50–73.

82.

Rath

S.K.

et al., Analysis and modeling of a safety critical system using petri-net model, In 2016 1st India International Conference on Information Processing (IICIP), IEEE, 2016, pp. 1–6.

83.

Reisig

, A primer in Petri net design, Springer Science & Business Media, 2012.

84.

Renault

Kordon

and Hugues

, Adapting models to model checkers, a case study: Analysing aadl using time or colored petri nets, In Rapid System Prototyping, 2009. RSP’09. IEEE/IFIP International Symposium on, IEEE, 2009, pp. 26–33.

85.

Renault

Kordon

and Hugues

, From aadl architectural models to petri nets: Checking model viability, In Object/Component/Service-Oriented Real-Time Distributed Computing, 2009. ISORC’09. IEEE International Symposium on, IEEE, 2009, pp. 313–320.

86.

Risler

and von Stryk

, Formal behavior specification of multi-robot systems using hierarchical state machines in xabsl, In AAMAS08-workshop on formal models and methods for multi-robot systems, Estoril, Portugal. Citeseer, 2008.

87.

Satchidananda

Susmita

and Sung-bae

, Integration of swarm intelligence and artificial neural network, volume 78, World Scientific, 2011.

88.

Silva

Gonçalves

Dimuro

and de Manuel Jerez

, Modeling agent periodic routines in agent-based social simulation using colored petri nets, In 2013 BRICS Congress on Computational Intelligence and 11th Brazilian Congress on Computational Intelligence, IEEE, 2013, pp. 644–650.

89.

Šimoňák

and Tomášek

, Acp semantics for petri nets, Computing and Informatics 37(6) (2019), 1464–1484.

90.

Singh

L.K.

and Rajput

, Dependability analysis of safety critical real-time systems by using petri nets, IEEE Transactions on Control Systems Technology 26(2) (2017), 415–426.

91.

Skobelev

, Multi-agent systems for real-time adaptive resource management, In Industrial Agents, Elsevier, 2015, pp. 207–229.

92.

Smaali

Choutri

and Belala

, K semantics for dynamic software architectures, In Proceedings of the International Arab Conference on Information Technology (ACIT ’2013), 2013.

93.

Souri

and Navimipour

N.J.

, Behavioral modeling and formal verification of a resource discovery approach in grid computing, Expert Systems with Applications 41(8) (2014), 3831–3849.

94.

Stehr

M.-O.

Meseguer

and Ölveczky

P.C.

, Rewriting logic as a unifying framework for petri nets, In Unifying Petri Nets, Springer, 2001, pp. 250–303.

95.

Subburaj

V.H.

and Urban

J.E.

, Applying formal methods to specify security requirements in multi-agent systems, In 2018 Federated conference on computer science and information systems (FedCSIS), IEEE, 2018, pp. 707–714.

96.

Subburaj

V.H.

and Urban

J.E.

, Specifying security requirements in multi-agent systems using the descartes-agent specification language and auml, In Information technology for management: Emerging research and applications, Springer, 2018, pp. 93–111.

97.

van der Aalst

and Best

, Application and Theory of Petri Nets and Concurrency: 38th International Conference, PETRI NETS 2017, Zaragoza, Spain, June 25–30 2017, Proceedings, volume 10258. Springer, 2017.

98.

van Riemsdijk

M.B.

Aştefănoaei

and de Boer

F.S.

, Using the maude term rewriting language for agent development with formal foundations, In Specification and Verification of Multi-agent Systems, Springer, 2010, pp. 255–287.

99.

Van Riemsdijk

M.B.

De Boer

F.S.

Dastani

and Meyer

J.-J.C.

, Prototyping 3apl in the maude term rewriting language, In International Workshop on Computational Logic in Multi-Agent Systems, Springer, 2006, pp. 95–114.

100.

Wang

Shen

and Zhu

, Agent oriented programming based on slabs, In Computer Software and Applications Conference, 2005. COMPSAC 2005. 29th Annual International, volume 1, IEEE, 2005, pp. 127–132.

101.

Wendt

Wilker

Meisel

and Sauter

, A multi-agent-based middleware for the development of complex architectures, In 2018 IEEE 27th International Symposium on Industrial Electronics (ISIE), IEEE, 2018, pp. 723–728.

102.

Wolf

, Petri net model checking with lola 2, In International Conference on Applications and Theory of Petri Nets and Concurrency, Springer, 2018, pp. 351–362.

103.

Wooldridge

Fisher

Huget

M.-P.

and Parsons

, Model checking multi-agent systems with mable, In Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, ACM, 2002, pp. 952–959.

104.

Yang

and Pi

, Towards a formal semantics for the aadl behavior annex, In Design, Automation & Test in Europe Conference & Exhibition, 2009. DATE’09, IEEE, 2009, pp. 1166–1171.

105.

Yeung

W.L.

, Behavioral modeling and verification of multi-agent systems for manufacturing control, Expert Systems with Applications 38(11) (2011), 13555–13562.

106.

and Cai

, Object-oriented petri nets based architecture description language for multi-agent systems, IJCSNS 6(1) (2006), 123–131.

107.

Zhang

Y.-H.

Fan

J.-C.

and Liao

X.-l.

, Simulation method of command and control process based on petri net [j], Journal of System Simulation 7 (2012).

108.

Zhu

Hall

and May

, Software unit test coverage and adequacy, ACM Computing Surveys 29(4) (1997), 366–427.

109.

Zoumpoulaki

Avradinis

and Vosinakis

, A multi-agent simulation framework for emergency evacuations incorporating personality and emotions, In Hellenic Conference on Artificial Intelligence, Springer, 2010, pp. 423–428.

110.

Zurita

N.F.S.

Colby

M.K.

Tumer

I.Y.

Hoyle

and Tumer

, Design of complex engineered systems using multi-agent coordination, Journal of Computing and Information Science in Engineering 18(1) (2018), 011003.

Petri net and rewriting logic based formal analysis of multi-agent based safety-critical systems

Abstract

Keywords

1. Introduction

1.1 Motivation

2.1 Specification approaches

2.2 Verification approaches

Table 1 Summary of works using model-checkers for MAS verification

3.1 Modeling stage

3.2 Specification stage

Table 2 Meaning of Petri net places and transitions

4.1 System description and modeling

4.2 System and properties specification

4.2.1 System specification

4.2.2 Properties specification

6. Conclusion and future work

Footnotes

Authors’ Bios

References

Table 1
Summary of works using model-checkers for MAS verification

Table 2
Meaning of Petri net places and transitions