<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>Software systems are becoming complex and dynamic with the passage of time, and to provide better fault tolerance and resource management they need to have the ability of self-adaptation. Multi-agent systems paradigm is an active area of research for modeling real-time systems. In this research, we have proposed a new agent named SA-ARTIS-agent, which is designed to work in hard real-time temporal constraints with the ability of self-adaptation. This agent can be used for the formal modeling of any self-adaptive real-time multi-agent system. Our agent integrates the MAPE-K feedback loop with ARTIS agent for the provision of self-adaptation. For an unambiguous description, we formally specify our SA-ARTIS-agent using Time-Communicating Object-Z (TCOZ) language. The objective of this research is to provide an intelligent agent with self-adaptive abilities for the execution of tasks with temporal constraints. Previous works in this domain have used Z language which is not expressive to model the distributed communication process of agents. The novelty of our work is that we specified the non-terminating behavior of agents using active class concept of TCOZ and expressed the distributed communication among agents. For communication between active entities, channel communication mechanism of TCOZ is utilized. We demonstrate the effectiveness of the proposed agent using a real-time case study of traffic monitoring system.</p>
</abstract>

Software systems are becoming complex and dynamic with the passage of time, and to provide better fault tolerance and resource management they need to have the ability of self-adaptation. Multi-agent systems paradigm is an active area of research for modeling real-time systems. In this research, we have proposed a new agent named SA-ARTIS-agent, which is designed to work in hard real-time temporal constraints with the ability of self-adaptation. This agent can be used for the formal modeling of any self-adaptive real-time multi-agent system. Our agent integrates the MAPE-K feedback loop with ARTIS agent for the provision of self-adaptation. For an unambiguous description, we formally specify our SA-ARTIS-agent using Time-Communicating Object-Z (TCOZ) language. The objective of this research is to provide an intelligent agent with self-adaptive abilities for the execution of tasks with temporal constraints. Previous works in this domain have used Z language which is not expressive to model the distributed communication process of agents. The novelty of our work is that we specified the non-terminating behavior of agents using active class concept of TCOZ and expressed the distributed communication among agents. For communication between active entities, channel communication mechanism of TCOZ is utilized. We demonstrate the effectiveness of the proposed agent using a real-time case study of traffic monitoring system.

Intelligent agent for formal modelling of temporal multi-agent systems

International Journal on Smart Sensing and Intelligent Systems

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

running-head

Software systems are becoming complex and dynamic with the passage of time, and to provide better fault tolerance and resource management they need to have the...

Query	Formula	Result
Is MTM3 signal’s green light working?	EF (MTM Signal.MTM3 Red=0 and MTM Signal.MTM3 Yellow=0 and MTM Signal.MTM3 Green=1)	Satisfied
Is MTM3 signal’s yellow light working?	EF (MTM Signal.MTM3 Red=0 and MTM Signal.MTM3 Yellow=1 and MTM Signal.MTM3 Green=0)	Satisfied
Is MTM3 signal’s red light working?	EF (MTM Signal.MTM3 Red=1 and MTM Signal.MTM3 Yellow=0 and MTM Signal.MTM3 Green=0)	Satisfied
Is MTM4 signal working?	EF ((MTM Signal.MTM4 Red=1and MTM Signal.MTM4 Yellow=0 and MTM Signal.MTM4 Green=0) or (MTM Signal.MTM4 Red=0 and MTM Signal.MTM4 Yellow=1 and MTM Signal.MTM4 Green=0) or (MTM Signal.MTM4 Red=0 and MTM Signal.MTM4 Yellow=0 and MTM Signal.MTM4 Green=1))	Satisfied
Is MTM4 signal’s green light working?	EF (MTM Signal.MTM4 Red=0 and MTM Signal.MTM4 Yellow=0 and MTM Signal.MTM4 Green=1)	Satisfied
Is MTM4 signal’s yellow light working?	EF (MTM Signal.MTM4 Red=0 and MTM Signal.MTM4 Yellow=1 and MTM Signal.MTM4 Green=0)	Satisfied
Is MTM4 signal’s red light working?	EF (MTM Signal.MTM4 Red=1 and MTM Signal.MTM4 Yellow=0 and MTM Signal.MTM4 Green=0)	Satisfied

Intelligent agent for formal modelling of temporal multi-agent systems

Article Category: Research-Article

Pubblicato online: 05 feb 2020

Pagine: 1 - 13

Ricevuto: 10 dic 2019

DOI: https://doi.org/10.21307/ijssis-2020-003

Parole chiave
Formal methods, Self-adaptation, Autonomic computing, Multi-agent systems, Real-time systems, TCOZ

© 2020 Awais Qasim et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Figure 1:

Figure 2:

Figure 3:

Figure 4:

Figure 5:

Formal verification of the traffic monitoring system.

Intelligent agent for formal modelling of temporal multi-agent systems

Article Category: Research-Article

Pubblicato online: 05 feb 2020

Pagine: 1 - 13

Ricevuto: 10 dic 2019

DOI: https://doi.org/10.21307/ijssis-2020-003

Parole chiaveFormal methods, Self-adaptation, Autonomic computing, Multi-agent systems, Real-time systems, TCOZ

© 2020 Awais Qasim et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Figure 1:

Figure 2:

Figure 3:

Figure 4:

Figure 5:

Formal verification of the traffic monitoring system.

Parole chiave
Formal methods, Self-adaptation, Autonomic computing, Multi-agent systems, Real-time systems, TCOZ