Formal requirement and architecture specifications of a multi-agent robotic system

TL;DR

This paper presents a formal approach for specifying and architecting multi-agent robotic systems, emphasizing step-wise refinement from abstract to concrete levels to ensure correctness and support analysis of functional and non-functional properties.

Contribution

It introduces a formal specification framework supporting systematic refinement and analysis, demonstrated through a case study, enhancing the reliability of complex multi-agent robotic systems.

Findings

Formal specifications facilitate analysis of system properties.

Step-wise refinement improves system correctness.

Case study validates the approach.

Abstract

One of the most challenging tasks in specification engineering for a multi-agent robotic system is to formally specify and architect the system, especially as a multi-agent robotic system is concurrent having concurrent processing, and often having dynamic environment. The formal requirement and architecture specifications along with step-wise refinement from abstract to concrete concepts play major role in formalizing the system. This paper proposes the formal requirement and architecture specifications aspects of an approach that supports analysis with respect to functional as well as non-functional properties by step-wise refinement from abstract to concrete specifications and formal architecture definition. These formal specifications have been exemplified by a case study. As formal specification techniques are getting more mature, our capability to build a correct complex multi-agent robotic system also grows quickly.