RoboArch: Architectural Modelling for Robotic Applications

Robotic systems are being employed in a diverse range of applications, with both the scale and complexity of their software increasing through having to operate in unstructured environments and to provide higher levels of autonomy. In addition, the need for robotic systems to be verified grows as robots are used in applications where they can have significant safety implications. Verification of even small robotic systems software is a challenging problem. Therefore, additional techniques are required to enable the practitioners to produce verified robotic systems. The use of model-driven engineering and domain-specific languages (DSLs) have proven useful in the development of complex systems in other areas so applying them to the field of robotics can contribute to the goal of building reliable and safe systems. In this thesis we present RoboArch, a notation for describing the architectures and patterns of robotic systems software supported by the formally defined semantics of RoboChart. RoboChart is a DSL for modelling the behaviour of robot software controllers using state machines. We describe RoboArch from the top-down. First, we examine the role of robotics software architectures in the development of robotic systems by reviewing five robotics architectures, and five DSLs. Next, for the layered architectural pattern, the RoboArch notation is introduced; we provide a metamodel, well-formedness conditions, and transformation rules to RoboChart. Further, we characterise two patterns: reactive skills and subsumption, which can be used by a layer. Finally, we discuss a tool and its implementation for the evaluation of RoboArch and automation of the rules as model transformations. We use a case study of a small obstacle avoidance system to demonstrate: the application of the reactive skills pattern using RoboArch and the expected properties of the architecture that can be proven using the generated RoboChart model CSP semantics.