Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> Model-based' design and automated code generation are being used increasingly at NASA. Many NASA projects now use MathWorks Simulink and Real- Time Workshop for at least some of their modeling and code development. The trend is to move beyond simulation and prototyping to actual flight code, particularly in the Guidance, Navigation, and Control domain. However, there are substantial obstacles to more widespread adoption of code generators in such safety-critical domains. Since code generators are typically not qualified, there is no guarantee that their output is correct, and consequently the generated code still needs to be fully tested and certified. Moreover, the regeneration of code can require complete recertification, which offsets many of the advantages of using a generator. Indeed, manual review of autocode can be more challenging than for hand-written code. Since the direct V&V of code generators is too laborious and complicated due to their complex (and often proprietary) nature, we have developed a generator plug-in to support the subsequent certification of the code that is generated. Specifically, the AutoCert tool supports certification by formally verifying that the generated code is free of different safety violations, by constructing an independently verifiable certificate, and by explaining its analysis in a textual form suitable for code reviews. This enables missions to obtain assurance about the safety and reliability of the code without excessive manual V&V effort and, as a consequence, increases the acceptance of code generators in safety-critical contexts. The generation of explicit certificates and textual reports is particularly well-suited to supporting independent V&V. The key technical idea of our approach is to exploit the idiomatic nature of auto-generated code in order to automatically infer logical annotations. These allow the automatic formal verification of the safety properties without requiring access to the internals of the code generator. The approach is independent of the particular generator used but is currently being adapted to code generated using MathWorks Real-Time Workshop, an automatic code generator that translates from Simulink/Stateflow models into embedded C code. <s> BIB001 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> Abstract : The design, prototype implementation, and demonstration of an ethical governor capable of restricting lethal action of an autonomous system in a manner consistent with the Laws of War and Rules of Engagement is presented. <s> BIB002 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> In this paper we assess the feasibility of using formal methods, and model checking in particular, for the certification of Unmanned Aircraft Systems (UAS) within civil airspace. We begin by modelling a basic UAS control system in PROMELA, and verify it against a selected subset of the CAA's Rules of the Air using the SPIN model checker. Next we build a more advanced UAS control system using the autonomous agent language Gwendolen, and verify it against the small subset of the Rules of the Air using the agent model checker AJPF. We introduce more advanced autonomy into the UAS agent and show that this too can be verified. Finally we compare and contrast the various approaches, discuss the paths towards full certification, and present directions for future research. <s> BIB003 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> A safety case is a structured argument, supported by a body of evidence, which provides a convincing and valid justification that a system is acceptably safe for a given application in a given operating environment. This report describes the development of a fragment of a preliminary safety case for the Swift Unmanned Aircraft System. The construction of the safety case fragment consists of two parts: a manually constructed system-level case, and an automatically constructed lower-level case, generated from formal proof of safety-relevant correctness properties. The authors provide a detailed discussion of the safety considerations for the target system, emphasizing the heterogeneity of sources of safety-relevant information, and use a hazard analysis to derive safety requirements, including formal requirements. The safety case is evaluated using three classes of metrics for measuring degrees of coverage, automation, and understandability. Preliminary conclusions are presented along with suggestions for future work. <s> BIB004 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> As humans are being progressively pushed further downstream in the decision-making process of autonomous systems, the need arises to ensure that moral standards, however defined, are adhered to by these robotic artifacts. While meaningful inroads have been made in this area regarding the use of ethical lethal military robots, including work by our laboratory, these needs transcend the warfighting domain and are pervasive, extending to eldercare, robot nannies, and other forms of service and entertainment robotic platforms. This paper presents an overview of the spectrum and specter of ethical issues raised by the advent of these systems, and various technical results obtained to date by our research group, geared towards managing ethical behavior in autonomous robots in relation to humanity. This includes: 1) the use of an ethical governor capable of restricting robotic behavior to predefined social norms; 2) an ethical adaptor which draws upon the moral emotions to allow a system to constructively and proactively modify its behavior based on the consequences of its actions; 3) the development of models of robotic trust in humans and its dual, deception, drawing on psychological models of interdependence theory; and 4) concluding with an approach towards the maintenance of dignity in human-robot relationships. <s> BIB005 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and theorem proving techniques that describe and formally verify the robot’s discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty. <s> BIB006 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> The use of unmanned aircraft for civil applications is expected to increase over the next decade, particularly in so-called dull, dirty, and dangerous missions. Unmanned aircraft will undoubtedly require some form of autonomy to ensure safe operations for all airspace users. However, to be used for civil applications, unmanned aircraft must gain regulatory approval in a process known as “certification”. This paper presents a proof-of-concept approach to the generation of certification evidence for autonomous unmanned aircraft based on a combination of formal verification and flight simulation. In particular, a class of autonomous systems controlled by rational agents is examined, and we give examples of 23 different properties, based on the rules of the air and notions of airmanship, which can be used in the formal model checking of rational agents controlling autonomous unmanned aircraft. Our techniques can be based on either 1) implicit models of the aircraft’s physical environment specified in terms of... <s> BIB007 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> Software is an essential part of robotic systems. As robots and autonomous systems are more and more deployed in human environments, we need to use elaborate validation and verification techniques in order to gain a higher level of trust in our systems. This motivates our determination to apply formal verification methods to robotics software. In this paper, we describe our results obtained using model-checking on the functional layer of an autonomous robot. We implement an automatic translation from GenoM, a robotics model-based software engineering framework, to the formal specification language Fiacre. This translation takes into account the semantics of the robotics middleware. TINA, our model-checking toolbox, can be used on the synthesized models to prove real-time properties of the functional modules implementation on the robot. We illustrate our approach using a realistic autonomous navigation example. <s> BIB008 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> Abstract Autonomous systems such as unmanned vehicles are beginning to operate within society. All participants in society are required to follow specific regulations and laws. An autonomous system cannot be an exception. Inevitably an autonomous system will find itself in a situation in which it needs to not only choose to obey a rule or not, but also make a complex ethical decision. However, there exists no obvious way to implement the human understanding of ethical behaviour in computers. Even if we enable autonomous systems to distinguish between more and less ethical alternatives, how can we be sure that they would choose right? We consider autonomous systems with a hybrid architecture in which the highest level of reasoning is executed by a rational (BDI) agent. For such a system, formal verification has been used successfully to prove that specific rules of behaviour are observed when making decisions. We propose a theoretical framework for ethical plan selection that can be formally verified. We implement a rational agent that incorporates a given ethical policy in its plan selection and show that we can formally verify that the agent chooses to execute, to the best of its beliefs, the most ethical available plan. <s> BIB009 </s> Formal Specification and Verification of Autonomous Robotic Systems: A Survey <s> Evidence for Certification and Trust <s> The Care-O-bot is an autonomous robotic assistant that can support people in domestic and other environments. The behaviour of the robot can be defined by a set of high level control rules. The adoption and further development of such robotic assistants is inhibited by the absence of assurances about their safety. In previous work, formal models of the robot behaviour and its environment were constructed by hand and model checkers were then used to check whether desirable formal temporal properties were satisfied for all possible system behaviours. In this paper we describe the details of the software CRutoN, that provides an automatic translation from sets of robot control rules into input for the model checker NuSMV. We compare our work with previous attempts to formally verify the robot control rules, discuss the potential applications of the approach, and consider future directions of research. <s> BIB010
Robotic systems are frequently deployed in safety-critical domains, such as nuclear or aerospace. These systems require certification, and each domain usually has a specific certification body. Ensuring that the engineering techniques used for developing robotic systems are able to provide appropriate certification evidence is thus essential. However, autonomous robotic systems development often falls short of providing sufficient evidence, or evidence in the correct form, for these certification bodies BIB008 . When certifying a piloted aircraft, the certification bodies assume that it will have a suitably qualified and competent crew in control. When an autonomous system is in control of a pilotless aircraft, this system must also be certified. However, the regulatory requirements for such a pilotless aircraft are still under development BIB007 . Choosing an appropriate formal method for a particular system is no mean feat as there are currently no standard guidelines available to aid developers in choosing the most suitable approach  . In fact, one of the main difficulties here is in choosing a formalism so that a good compromise is reached between how expressive the formalism is and the complexity of its analysis/synthesis algorithms  . This also presents a challenge for certification bodies that need to be able to determine the reliability of safety-critical robotic systems and the formal methods that were employed during development. Autonomous vehicles are usually regulated by the relevant vehicle authority for the territory they are used in. However, their introduction also requires public trust. The majority of respondents of a recent survey on public attitudes toward driverless cars (United Kingdom, United States, and Australia) had both a high expectation of their benefits and a high level of concern over their safety and security  . In contrast to the nuclear and aerospace domains, robots used in domestic or care environments do not have strong certification requirements but must be shown to be safe and trustworthy. This covers both safety and the public perception of safety; notions of usability and reliability; and a perception that the robot will not do anything unexpected, unsafe, or unfriendly  . This lack of both trust and safety assurances can hamper adoption of robotic systems in wider society BIB010 , even where they could be extremely useful and potentially improve the quality of human life. Isabelle/HOL and temporal logic have been used to formalize a subset of traffic rules for vehicle overtaking in Germany  . As we move toward driverless cars, a key concern is enumerating how much one robot needs to know about the goals and constraints of other vehicles on the road to not be considered at blame for any accident BIB006 . In related work, Webster et al. BIB003 utilize model checking to provide certification evidence for an autonomous pilotless aircraft system using the Gwendolen agent language and the Agent Java PathFinder (AJPF) approach as an improvement over Promela and SPIN. The certification process often requires safety cases that provide a structured argument of a system's safety in a certain context, given certain assumptions. Automating safety case generation is challenging; safety cases must combine elements of the physical design, software design, and the maintenance of both. Denney and Pai BIB004 have described a methodology for automatically generating safety cases for the Swift pilotless aircraft system using a domain theory and their AutoCert tool BIB001 , which automates the generation of safety case fragments. Related to trust is the issue of ethical robotic behavior. Several approaches to constraining the behavior of a robotic or autonomous system have focused on the distinction between ethical and nonethical choices BIB002 BIB005  . Worryingly, they ignore the potential situation where no ethical choice is available, and there seems to be little consideration of this situation in the literature BIB009 . Clearly, reasoning about ethical behaviour is at least as difficult with robots as it is with humans.