3A1-G08 An AADL model of the control architecture for a safe robot wheelchair(Robotics with Safety and Reliability)
Geoffrey Biggs, Kiyoshi Fujiwara, Keiju Anada · The Proceedings of JSME annual Conference on Robotics and Mechatronics (Robomec) · 2014
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 model of a redundant control architecture for a mobile robot. The model is specified using the Architecture Analysis and Design Language (AADL). This formal language allows the model to be analysed to prove system properties such as sufficient processor capacity and control latency. We present the results of a model completeness analysis, a processor capacity analysis, and a latency analysis.