Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Set-Based Formalisms <s> This paper presents a formal specification-based software monitoring approach that can dynamically and continuously monitor the behaviors of a target system and explicitly recognize undesirable behaviors in the implementation with respect to its formal specification. The key idea of our approach is in building a monitoring module that connects a specification animator with a program debugger. The requirements information about expected dynamic behaviors of the target system are gathered from the formal specification animator, while the actual behaviors of concrete implementations of the target system are obtained through the program debugger. Based on the information obtained from both sides, the judgement on the conformance of the concrete implementation with respect to the formal specification is made timely while the target system is running. Furthermore, the proposed formal specification-based software monitoring technique does not embed any instrumentation codes to the target system nor does it annotate the target system with any formal specifications. It can detect implementation errors in a real-time manner, and help the developers and users of the system to react to the problems before critical failure occurs. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Set-Based Formalisms <s> Self-adaptive software systems are an emerging class of systems that adjust their behavior at runtime to achieve certain functional or quality of service objectives. The construction of such systems has shown to be significantly more challenging than traditional systems, partly because researchers and practitioners have been struggling with the lack of a precise method of describing, comparing, and evaluating alternative architectural choices. In this paper, we introduce a reference model, entitled FOrmal Reference Model for Self-adaptation (FORMS), which intends to alleviate this pressing issue. FORMS consists of a small number of formally specified modeling primitives that correspond to the key variation points within self-adaptive software systems, and a set of relationships that guide their composition. We present our experiences with applying FORMS to several existing systems, which not only demonstrates its ability to precisely illuminate their underlying characteristics, but also its potential as a method of rigorously specifying architectural patterns for this domain. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Set-Based Formalisms <s> A practical text suitable for an introductory or advanced course in formal methods, this book presents a mathematical approach to modelling and designing systems using an extension of the B formal method: Event-B. Based on the idea of refinement, the author's systematic approach allows the user to construct models gradually and to facilitate a systematic reasoning method by means of proofs. Readers will learn how to build models of programs and, more generally, discrete systems, but this is all done with practice in mind. The numerous examples provided arise from various sources of computer system developments, including sequential programs, concurrent programs and electronic circuits. The book also contains a large number of exercises and projects ranging in difficulty. Each of the examples included in the book has been proved using the Rodin Platform tool set, which is available free for download at www.event-b.org. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Set-Based Formalisms <s> Ensuring fault tolerance of satellite systems is critical for achieving goals of the space mission. Since the use of redundancy is restricted by the size and the weight of the on-board equipments, the designers need to rely on dynamic reconfiguration in case of failures of some components. In this paper we propose a formal approach to development of dynamically reconfigurable systems in Event-B. Our approach allows us to build the system that can discover possible reconfiguration strategy and continue to provide its services despite failures of its vital components. We integrate probabilistic verification to evaluate reconfiguration alternatives. Our approach is illustrated by a case study from aerospace domain. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Set-Based Formalisms <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> BIB005
Set-based formalisms (such as the B-Method and Z) specify a system using set-theoretic representation and manipulation of data. They are well suited to capturing complicated data structures but usually only provide limited, if any, features for capturing behavior. As mentioned in Section 4.3, self-adaptive (or reconfigurable) behavior is often key for autonomous robotic systems. Weyns et al. describe a formal reference model for self-adaptive systems, called FORMS BIB002 , which provides a Z model that describes an arbitrary self-adaptive system. They suggest that this model could be used in conjunction with various existing tools to type check the adaptations to ensure that they are valid, visualize the model using animators, automatically generate test cases, or transform the model into other notations for other types of analysis. The model provides a method of describing a self-adaptive system to enable communication about the adapting architecture during system design and comparison of different architectural configurations. Liang et al. BIB001 use the Java animator for Z specifications, combined with a Java debugger, to provide a runtime monitoring system. A Z specification describes the system's behavior, which is animated and compared to the running program via the jdb Java debugger to check that the running program implements the Z specification. They demonstrate this approach on a robotic assembly system, designed to build robots for the NASA ANTS project. BIB005 Two advantages of combining the Z animator with a Java debugger are that it keeps the monitor and program code separate and that the approach doesn't require any alterations to the monitored program. In BIB004 , Event-B specifications are combined with probabilistic properties to derive reconfigurable architectures for an on-board satellite system. Event-B evolved from the B-Method and is more suitable to modeling the dynamic behavior of a system than its predecessor BIB003 . The combination of these formalisms allows the models of reconfigurations to be checked using PRISM for both the derivation (via refinement) of the system from its specification and the probabilistic assessment of their reliability and performance.