Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> MDE/XML: Numerous Model-Driven Engineering (MDE) approaches use the Eclipse Modeling <s> A key part of programming a robotic system is specifying the responses to events that the robot may encounter. Existing methods of programming responses include event loops, reactive languages and hybrid architectures, none of which meet the specific needs of mobile robot programming. This work presents a design for new semantics for specifying reactivity in mobile robot programs, one that allows for effective specification of reactive behaviour within procedural robot programs. An initial evaluation version is implemented in Python. Events and responses are supported as program objects, and are connected together by new statements. Programmers specify connections between events and responses anywhere within the program code, so connections can easily be changed in response to changes in program and robot state. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> MDE/XML: Numerous Model-Driven Engineering (MDE) approaches use the Eclipse Modeling <s> Engineering software for robotics applications requires multi-domain solutions. Model-driven development (MDD) promises efficient means for developing domain-specific and reusable models of robotics software. Code generators transform these models into executable code for specific robotic platforms. Robotics is heterogeneous and robotics applications pose various challenges to leveraging the potential of MDD. Combinations of modeling languages and platforms are often problem-specific. Generative software development for multi-domain applications requires both the effective integration of modeling languages and composition of code generators. We present the extensible MontiArcAutomaton architecture modeling framework for the generative development of robotics applications with a strong focus on language integration and generator composition. Its core modeling language is a component & connector architecture description language that can be extended with problem-specific component behavior modeling languages. ::: We present how MontiArcAutomaton supports syntactic and semantic behavior modeling language integration to describe component behavior in most suitable modeling languages and code generator composition to synthesize code from integrated models. We sketch a process for model-driven development of robotics applications using MontiArcAutomaton. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> MDE/XML: Numerous Model-Driven Engineering (MDE) approaches use the Eclipse Modeling <s> One of the major investment for applying industrial robots in production resides in the software development, which is an interdisciplinary and heterogeneous engineering process. This paper presents a novel model-driven approach that uses AutomationML as modeling framework and ontological reasoning as inference framework for constructing robotic application using Robot Operating System (ROS). We show how different robotic components can be classified and modeled with AutomationML, how these components can be composed together to a production system, and how the AutomationML models can be processed semantically by utilizing Semantic Web technologies and ontological reasoning. By applying model-to-text transformation techniques, executable ROS code can be generated from the models that foster fast prototyping and the reuse of robotic software. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> MDE/XML: Numerous Model-Driven Engineering (MDE) approaches use the Eclipse Modeling <s> Safety is a key challenge in robotics, in particular for mobile robots operating in an open and unpredictable environment. To address the safety challenge, various software-based approaches have been proposed, but none of them provide a clearly specified and isolated safety layer. In this paper, we propose that safety-critical concerns regarding the robot software be explicitly declared separately from the main program, in terms of externally observable properties of the software. Concretely, we use a Domain-Specific Language (DSL) to declaratively specify a set of safety-related rules that the software must obey, as well as corresponding corrective actions that trigger when rules are violated. Our DSL, integrated with ROS, is shown to be capable of specifying safety-related constraints, and is experimentally demonstrated to enforce safety behaviour in existing robot software. We believe our approach could be extended to other fields to similarly simplify safety certification. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> MDE/XML: Numerous Model-Driven Engineering (MDE) approaches use the Eclipse Modeling <s> Despite the existence of powerful formal languages for writing robot controllers, most existing functional modules are written using standard programming languages. The existence of such a code base raises critical challenges: 1. How to enable automated analysis, monitoring, and reuse of existing code given that reasoning directly about code fragments is impractical. 2. How to convey to users the expected level of performance of an autonomous robot? 3. Perhaps most crucial: how to quickly identify abnormal behavior of autonomous robots? This is a key impediment to the deployment of such platforms in open environments. We address these issues through the use of performance-level profiles (PLPs), a formal, yet intuitive, language for specifying the expected properties of functional modules, designed with the above aims in mind. PLPs are motivated by action specification languages, such as PDDL 2.1, but add novel elements important for robotic applications, such as update frequency, run-time statistics, progress measures, and trigger conditions, and take into account the different roles modules can play. PLPs have been used to support monitoring in two projects: an autonomous compact track loader, and a service robot. Additionally, we developed a number of tools for automated monitoring-code generation from PLPs. <s> BIB005
Framework's Ecore meta-meta-model  . The work in BIB003 presents a mapping from the XMLbased AutomationML into ROS program code. The BRICS Component Model  translates highlevel models into platform-specific component models for Orocos and ROS. Another model-driven approach is the MontiArcAutomaton architecture description language BIB002 , which translates models into program code, mostly for ROS BIB004 . Performance Level Profiles BIB005 is an XML-based language for describing the expected properties of functional modules. They provide tools for the automatic generation of code for runtime monitoring of described properties. They again target the ROS framework, but the output from their tool is flexible and not tied to ROS. RADAR is a novel procedural language, with a Python implementation, for describing robot event responses BIB001 . Discussion: Middleware frameworks provide a flexible standard interface to the robotic hardware, and the above non-and semiformal approaches aim to adapt the parts of software engineering practice that are relevant to the robotics domain. DSLs abstractly describe properties about specific parts of the system, often improving the understanding or interoperability of the system. Graphical notations aid in communication and visualization. However, more formal languages provide unambiguous semantics and enable reasoning about the whole program rather than only a particular set of program behaviors. Next, we describe the external challenges faced when applying formal methods to robotic systems. These challenges are external to the robotic system and are independent of the type of robotic system being developed.