Formal Evidence Generation for Assurance Cases for Robotic Software Models

Robotics and Autonomous Systems are increasingly deployed in safety-critical domains, so that demonstrating their safety is essential. Assurance Cases (ACs) provide structured arguments supported by evidence, but generating and maintaining this evidence is labour-intensive, error-prone, and difficult to keep consistent as systems evolve. We present a model-based approach to systematically generating AC evidence by embedding formal verification into the assurance workflow. The approach addresses three challenges: systematically deriving formal assertions from natural language requirements using templates, orchestrating multiple formal verification tools to handle diverse property types, and integrating formal evidence production into the workflow. Leveraging RoboChart, a domain-specific modelling language with formal semantics, we combine model checking and theorem proving in our approach. Structured requirements are automatically transformed into formal assertions using predefined templates, and verification results are automatically integrated as evidence. Case studies demonstrate the effectiveness of our approach.

Probabilistic relations for modelling epistemic and aleatoric uncertainty: its semantics and automated reasoning with theorem proving

Probabilistic programming is a programming paradigm that combines general computer programming, statistical inference, and formal semantics to help systems to made decisions when facing uncertainty. Probabilistic programs are ubiquitous and believed to have a major impact on machine intelligence. While many probabilistic algorithms have been used in practice in different domains, their automated verification based on formal semantics is still a relatively new research area. In the last two decades, it has been attracting a lot of interest. Many challenges, however, still remain. Our work presented in this paper, probabilistic relations, takes a step into our vision to tackle these challenges. Our work in essence is based on Hehner's predicative probabilistic programming, but there are several obstacles to the wider adoption of his work. Our contributions here include (1) the formalisation of its syntax and semantics by introducing an Iverson bracket notation to separate relations from arithmetic; (2) the formalisation of relations using Unifying Theories of Programming (UTP) and probabilities outside the brackets using summation over the topological space of the real numbers; (3) the constructive semantics for probabilistic loops using the Kleene's fixed point theorem; (4) the enrichment of its semantics from distributions to subdistributions and superdistributions in order to deal with the constructive semantics; (5) the unique fixed point theorem to largely simplify the reasoning about probabilistic loops; and (6) the mechanisation of our theory in Isabelle/UTP, an implementation of UTP in Isabelle/HOL, for automated reasoning using theorem proving. We demonstrate six interesting examples, and among them, one is about robot localisation, two are classification problems in machine learning, and two contain probabilistic loops.

New Opportunities for Integrated Formal Methods

Formal methods have provided approaches for investigating software engineering fundamentals and also have high potential to improve current practices in dependability assurance. In this article, we summarise known strengths and weaknesses of formal methods. From the perspective of the assurance of robots and autonomous systems~(RAS), we highlight new opportunities for integrated formal methods and identify threats to their adoption to be mitigated. Based on these opportunities and threats, we develop an agenda for fundamental and empirical research on integrated formal methods and for successful transfer of validated research to RAS assurance. Furthermore, we outline our expectations on useful outcomes of such an agenda.