文章基本信息

标题：Approach for the formal modeling of requirements, verification, and architecture of a multi-agent robotic system
本地全文：下载
作者：Nadeem Akhtar ; Anique Akhtar
期刊名称：International Journal of Computer Science Issues
印刷版ISSN：1694-0784
电子版ISSN：1694-0814
出版年度：2014
卷号：11
期号：1
出版社：IJCSI Press
摘要：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.
关键词：Architecture Description Language (ADL); Correctness properties; Formal architecture; Formal verification; Liveness property; Multi;Agent robotic system; Safety property.