Modelling and Analysis of a Redundant Mobile Robot Architecture Using AADL

As the complexity of robots deployed in the real world increases, the use of formal specifications in the development of safety-critical robot systems is becoming increasingly important. A formal specification gives confidence in the correctness, completeness, and accuracy of a system design. In this paper, we present a formal specification of a redundant control architecture for a mobile robot in the form of a model. The model is created using the Architecture Analysis and Design Language (AADL). This formal language allows the model to be analysed to prove system properties of interest. In this case, we are interested in proving the response time of the robot to external obstacles and to internal errors. We present the model and the results of these analyses with the goal of proving that the architecture is sufficiently safe for use in a safe robot wheelchair.

Authors and Affiliations

1. Intelligent Systems Research Institute, National Institute of Advanced Industrial Science and Technology (AIST), AIST Tsukuba Central 2, Tsukuba, Ibaraki, 305-8568, Japan

   Geoffrey Biggs & Kiyoshi Fujiwara

2. aRbot, Inc., Japan

   Keiju Anada

Editors and Affiliations

1. Department of Engineering, Università degli Studi di Bergamo, Viale Marconi 5, 24044, Dalmine, Italy

   Davide Brugali

2. Faculty EE-Math-CS, CTIT Institute, Robotics and Mechatronics Group, University of Twente, Room Carre 3437, P.O. Box 217, 7500 AE, Enschede, The Netherlands

   Jan F. Broenink

3. Artificial Intelligence Laboratory, Stanford University, 94305-9010, Stanford, CA, USA

   Torsten Kroeger

4. Faculty of Engineering, Electrical and Computer Engineering, Science Centre - Mathphysic, Level 2, University of Auckland, Room 303-249, 38 Princess Street, 1010, Auckland, New Zealand

   Bruce A. MacDonald

Reprints and permissions

© 2014 Springer International Publishing Switzerland

Policies and ethics