FORMAL SPECIFICATION AND VERIFICATION OF MULTI-AGENT ROBOTICS SOFTWARE SYSTEMS - A Case Study

Nadeem Akhtar, Yann Le Guyadec, Flavio Oquendo

2009

Abstract

One of the most challenging task in software specifications engineering for robotics multi-agent systems is to ensure correctness. As these systems have high concurrency, often have dynamic and distributed environments, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play major role in system correctness. Our objectives are the formal specification, analysis with respect to functional as well as non-functional properties by step-wise refinement from abstract to concrete specifications and then formal verification of these specifications. Multi-agent robotics systems are concurrent systems with processes working in parallel with synchronization between them. We have worked on Gaia multi-agent method along with finite state process based finite automata techniques and as a result we have defined the formal specifications of our system, checked the correctness and verified all possible flow of concurrent executions of these specifications. Our contribution consists in transforming Gaia organizational abstractions into executable FSP specifications that can be verified using LTS. We have considered a case study of our multi-agent robotics system to exemplify formal specifications and verification.

Paper Citation

in Harvard Style

Akhtar N., Le Guyadec Y. and Oquendo F. (2009). FORMAL SPECIFICATION AND VERIFICATION OF MULTI-AGENT ROBOTICS SOFTWARE SYSTEMS - A Case Study . In Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 1: ICAART, ISBN 978-989-8111-66-1, pages 475-482. DOI: 10.5220/0001657904750482

in Bibtex Style

@conference{icaart09,
author={Nadeem Akhtar and Yann Le Guyadec and Flavio Oquendo},
title={FORMAL SPECIFICATION AND VERIFICATION OF MULTI-AGENT ROBOTICS SOFTWARE SYSTEMS - A Case Study},
booktitle={Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 1: ICAART,},
year={2009},
pages={475-482},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0001657904750482},
isbn={978-989-8111-66-1},
}

in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 1: ICAART,
TI - FORMAL SPECIFICATION AND VERIFICATION OF MULTI-AGENT ROBOTICS SOFTWARE SYSTEMS - A Case Study
SN - 978-989-8111-66-1
AU - Akhtar N.
AU - Le Guyadec Y.
AU - Oquendo F.
PY - 2009
SP - 475
EP - 482
DO - 10.5220/0001657904750482