Contribution to the Formal Specification and Verification 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. Formal specifications based on model-checking are flexible, have a concrete syntax, and play vital role in correctness of a multi-agent robotic system. To formally verify safety and liveness of such systems is important because they have high concurrency and in most of the cases have dynamic environment. We have considered a case-study of a multi-agent robotic system for the transport of stock between storehouses to exemplify our formal approach. Our proposed development approach allows for formal verification during specification definition. The development process has been classified in to four major phases of requirement specifications, verification specifications, architecture specifications and implementation.

KitRobot: A multi-platform graphical programming IDE to program mini-robotic agents

The analysis, design and development of a graphical programming IDE for mini-robotic agents allows novice users to program robotic agents by a graphical drag and drop interface, without knowing the syntax and semantics of the intermediate programming language. Our work started with the definition of the syntax and semantics of the intermediate programming language. The major work is the definition of grammar for this language. The use of a graphical drag and drop interface for programming mini-robots offers a user-friendly interface to novice users. The user can program graphically by drag and drop program parts without having expertise of the intermediate programming language. The IDE is highly flexible as it uses xml technology to store program objects (i.e. loops, conditions) and robot objects (i.e. sensors, actuators). Use of xml technology allows making major changes and updating the interface without modifying the underlying design and programming.