Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> This paper studies a general methodology and an associated tool for translating AADL (Architecture Analysis and Design Language) and annex behavior specification into the BIP (Behavior Interaction Priority) language. This allows simulation of systems specified in AADL and application to these systems of formal verification techniques developed for BIP, e.g. deadlock detection. We present a concise description of AADL and BIP followed by the presentation of the translation methodology illustrated by a Flight Computer example. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> We present a methodology for modeling heterogeneous real-time components. ::: Components are obtained as the superposition of three layers : ::: Behavior, specified as a set of transitions; Interactions between transitions ::: of the behavior; Priorities, used to choose amongst possible interactions. ::: A parameterized binary composition operator is used to compose components layer by layer. ::: ::: We present the BIP language for the description and composition of layered components as well ::: as associated tools for executing and analyzing components on a dedicated platform. The language ::: provides a powerful mechanism for structuring interactions involving rendezvous and broadcast. ::: We show that synchronous and timed systems are particular classes of components. Finally, we ::: provide examples showing the utility of the BIP framework in heterogeneous component ::: modeling. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> This paper presents the behaviour-based control architecture iB2C ( i ntegrated B ehaviour- B ased C ontrol) used for the development of complex robotic systems. The specification of behavioural components is described as well as the integration of behaviour coordination and hierarchical abstraction. It is considered how the design process can be supported by guidelines and by tools for development as well as analysis. Finally some application platforms are presented. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> Autonomous robots are complex systems that require the interaction/cooperation of numerous heterogeneous software components. Nowadays, robots are critical systems and must meet safety properties including in particular temporal and real-time constraints. We present a methodology for modeling and analyzing a robotic system using the BIP component framework integrated with an existing framework and architecture, the LAAS Architecture for Autonomous System, based on GenoM. The BIP componentization approach has been successfully used in other domains. In this study, we show how it can be seamlessly integrated in the preexisting methodology. We present the componentization of the functional level of a robot, the synthesis of an execution controller as well as validation techniques for checking essential “safety” properties. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> Autonomous robots are complex systems that require the interaction/cooperation of numerous heterogeneous software components. Nowadays, robots are getting closer to humans and as such are becoming critical systems which must meet safety properties including in particular logical, temporal and real-time constraints. We present an evolution of the LAAS Architecture for Autonomous System and its tool GenoM. This evolution is based on the BIP (Behaviors Interactions Priorities) component based design framework which has been successfully used in other domains (e.g. embedded systems). In this study, we show how we seamlessly integrate BIP in the preexisting methodology. We present the componentization of the functional level of a robot, the synthesis of an execution controller as well as validation techniques for checking essential safety properties. This approach has been integrated in the LAAS architecture and we have performed a number of experiment in simulation but also on a real robot (DALA). <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> We present a computational framework for automatic synthesis of control and communication strategies for a robotic team from task specifications given as regular expressions about servicing requests in an environment. Our approach is based on two main ideas. First, we extend recent results from formal synthesis of distributed systems to check for the distributability of the task specification and to generate local specifications, while accounting for the service and communication capabilities of the robots. Second, by using a technique inspired from LTL model checking, we generate individual control and communication strategies. We illustrate the method with experimental results in our Robotic Urban-Like Environment. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> D-Finder 2 is a new tool for deadlock detection in concurrent systems based on effective invariant computation to approximate the effects of interactions among modules. It is part of the BIP framework, which provides various tools centered on a component-based language for incremental design. The presented tool shares its theoretical roots with a previous implementation, but was completely rewritten to take advantage of a new version of BIP and various new results on the theory of invariant computation. The improvements are demonstrated by comparison with previous work and reports on new results on a practical case study. <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> Verification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact in an heterogeneous environment. Those limitations entail the need for complementary verification methods such as runtime verification based on dynamic analysis and prone to scalability. In this paper, we integrate runtime verification into the BIP (Behavior, Interaction, and Priority) framework. BIP is a powerful component-based framework for the construction of heterogeneous systems. Our method augments BIP systems with monitors checking a user-provided specification. This method has been implemented in RV-BIP, a prototype tool that we used to validate the whole approach on a robotic application. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> We have recently started an effort to combine a state of the art tool for developing functional modules of robotic systems (G^e^noM) with a component based framework for implementing embedded real-time systems (BIP). Unlike some works which study the connection between formal approaches and the highest (decisional) level of the robot software architecture, where deliberative activities such as planning, diagnostics, and execution control are conducted, we tackle the problem of using formal methods for developing modules of the functional level of robots. Little attention has been drawn to the development of these modules whose robustness is paramount to the robustness of the overall platform. To this end, we have successfully developed the G^e^noM/BIP component based design approach and applied it to the functional level of a complex exploration rover. Here, we report on this work, and show how we: (i) produce a very fine grained formal computational model of the robot functional level; (ii) run the BIP engine on the real robot, which executes and enforces the model semantics at runtime; and (iii) check the model offline for deadlock-freedom, as well as other safety properties. Moreover, we also extended this paradigm in a number of promising directions: (i) introduced a real-time BIP engine which can now use and control a timed BIP model; (ii) distributed the model and the engine over multiple CPUs; (iii) proposed a user-friendly language for specifying constraints on the model; and (iv) linked the model with a temporal plan execution controller. Interestingly, although our approach was initially proposed for the lowest level of robot architectures, these more recent extensions now allow us to model and manage the deliberation taking place at the decisional layer. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> We present a computational framework for automatic synthesis of control and communication strategies for a robotic team from task specifications that are given as regular expressions about servicing requests in an environment. We assume that the location of the requests in the environment and the robot capacities and cooperation requirements to service the requests are known. Our approach is based on two main ideas. First, we extend recent results from formal synthesis of distributed systems to check for the distributability of the task specification and to generate local specifications, while accounting for the service and communication capabilities of the robots. Second, by using a technique that is inspired by linear temporal logic model checking, we generate individual control and communication strategies. We illustrate the method with experimental results in our robotic urban-like environment. <s> BIB010 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Frameworks for Verifiable Robotic Software <s> The challenges of pervasive and mobile computing environments, which are highly dynamic and unpredictable, have motivated the development of self-adaptive software systems. Although noteworthy successes have been achieved on many fronts, the construction of such systems remains significantly more challenging than traditional systems. We argue this is partially because researchers and practitioners have been struggling with the lack of a precise vocabulary for describing and reasoning about the key architectural characteristics of self-adaptive systems. Further exacerbating the situation is the fact that existing frameworks and guidelines do not provide an encompassing perspective of the different types of concerns in this setting. In this article, we present a comprehensive reference model, entitled FOrmal Reference Model for Self-adaptation (FORMS), that targets both issues. FORMS provides rigor in the manner such systems can be described and reasoned about. It consists of a small number of formally specified modeling elements that correspond to the key concerns in the design of self-adaptive software systems, and a set of relationships that guide their composition. We demonstrate FORMS's ability to precisely describe and reason about the architectural characteristics of distributed self-adaptive software systems through its application to several existing systems. FORMS's expressive power gives it a potential for documenting reusable architectural solutions (e.g., architectural patterns) to commonly encountered problems in this area. <s> BIB011
Our literature search revealed a number of frameworks for developing verifiable robotic systems. These frameworks often encompass a number of the techniques already described in Section 6, but frequently, they incorporate bespoke tools and formalisms. Although some facilitate the use of multiple verification techniques, we omit them from Section 6.4 since users are generally expected to apply only one of the available techniques in practice rather than integrating results from several. The BIP framework BIB002 is a toolset for modeling component-based real-time software, with a notation based on FSMs. The basic component of a BIP model is a state transition system, labeled with C/C++ functions. These components are combined to form larger components and models can be verified using the D-Finder tool BIB007 . In BIB009 , Abdellatif et al. combine the BIP framework with the G en oM robot software architecture to provide a technique that can synthesize robotic control software from BIP models of the required behavior. This enables the generation of robotic software, in G en oM, that is correct by construction. Abdellatif et al. show the generation of software for a wheeled rover robot using fault injection to test that the constraints in the BIP specification are enforced by the generated software. Other work along this vein includes a meta-model-based translation from the Architecture Analysis and Design Language (AADL) into BIP BIB001 . This facilitates simulation of AADL combined with formal verification using the model-checking tools in the BIP framework; in particular, this work uses the Aldebaran model checker. Furthermore, Falcone et al. BIB008 integrate runtime verification into the BIP framework. They describe their approach and a tool, RV-BIP, which generates monitors for BIP to check specifications at runtime. Related to this are attempts to integrate BIP and the LAAS architecture, which is based on G en oM BIB004 BIB005 . The Averest framework provides "tools for verifying temporal properties of synchronous programs" that are written in the Quartz language BIB003 . The Quartz programs are translated into Averest Interchange Format (AIF) and then verified against LTL specifications using the Beryl model checker or other third-party tools that have interfaces to them such as SMV. Furthermore, the framework has a code generation tool called Topaz that can output Verilog, VHDL, and C code. Chen et al. BIB010 BIB006 propose a computational framework for automatic synthesis of control and communication strategies for robot teams using task specifications that are written as regular expressions. Their objective is to "generate provably correct individual control and communication strategies" from regular expressions, which are used to create FSA. They demonstrate their approach using a Robotic Urban-Like Environment (RULE), where autonomous cars must navigate and avoid collisions. Their technique builds on LTL model checking and uses JFLAP and MatLab BIB006 . The FOrmal Reference Model for Self-adaptation (FORMS) provides a reference model that can guide developers as to how to formulate a Z specification of a self-adaptive system BIB011 . This is built upon MAPE-K and supports agents and formal refinement of specifications in Z. Kim et al.  use the Esterel framework to verify the stopping behavior of a home service robot. This framework offers facilities for specifying and verifying robotic systems using model checking. Esterel can also be translated into an associated C or C++ program, and the semantics of an Esterel program is given in terms of the FSM that it describes. To enable systems to be checked for temporal logic properties, the authors translate them into observers in Esterel.