Approach for the formal modeling of requirements, verification, and architecture of a multi-agent robotic system
It is important to have multi-agent robotic system specifications that ensure correctness properties of safety and liveness. As these systems have concurrency, and often have dynamic environment, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play a major role in system correctness. Formal verification is used for exhaustive investigation of the system space thus ensuring that undetected failures in the behavior are excluded. We construct the system incrementally from subcomponents, based on software architecture. The challenge is to develop a safe multi-agent robotic system, more specifically to ensure the correctness properties of safety and liveness. We have proposed a development approach that allows for formal verification and evaluation during specification definition. The development process has been classified in to four major phases of requirement specifications, verification specifications, architecture specifications and implementation. This paper presents an overview of this approach.
Keywords: Architecture Description Language (ADL), Correctness properties, Formal architecture, Formal verification, Liveness property, Multi-Agent robotic system, Safety property.
Download Full-Text
ABOUT THE AUTHORS
Nadeem Akhtar
Dr. Nadeem Akhtar is Assistant Professor at the Department of Computer Science & IT, The Islamia University of Bahawalpur. He completed his PhD from the research Lab. VALORIA of Computer Science, University of South Brittany (UBS), France in 2010. His research areas are formal specification, formal architecture, and service-oriented architecture for robotics.
Anique Akhtar
Anique Akhtar has a BS in Electrical Engineering from LUMS (Lahore University of Management Sciences). He is currently pursuing his MS Degree from KOC University, Istanbul Turkey.
Nadeem Akhtar
Dr. Nadeem Akhtar is Assistant Professor at the Department of Computer Science & IT, The Islamia University of Bahawalpur. He completed his PhD from the research Lab. VALORIA of Computer Science, University of South Brittany (UBS), France in 2010. His research areas are formal specification, formal architecture, and service-oriented architecture for robotics.
Anique Akhtar
Anique Akhtar has a BS in Electrical Engineering from LUMS (Lahore University of Management Sciences). He is currently pursuing his MS Degree from KOC University, Istanbul Turkey.
