We present a theorem-proving-based technique for verifying deadlock freedom of CSP-style concurrent models in Isabelle/HOL. The approach addresses challenges that are difficult to handle using model checking alone, including infinite state spaces, compositional reasoning in the presence of shared variables, and the need for mechanised proofs. Our main contribution is a coinductive characterisation of deadlock freedom that is equivalent to the standard CSP refinement-based definition, but is more amenable to automated reasoning in an interactive theorem prover. To support reasoning about shared variables, we introduce an assume–guarantee strategy that enforces invariants within transition semantics. The technique is generally applicable to CSP specifications that model shared variables using standard CSP constructs. In particular, we consider the semantics of RoboChart, a domain-specific modelling language for robotic control software, which we mechanise in Isabelle via a shallow embedding in HOL-CSP, and implement automated proof methods. The approach is evaluated on three case studies, including two RoboChart models of industrial robotic systems.

Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct formal proofs demonstrating satisfaction of certain critical properties in support of high-assurance software engineering. To ensure coherent results between execution and proof, we need unifying semantics and automation. In this article, we mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework. ITrees are coinductive structures that allow us to encode infinite labelled transition systems, yet they are inherently executable. We use ITrees to create verification tools for stateful imperative programs, concurrent programs with message passing in the form of the CSP and Circus languages, and abstract system models in the style of the Z and B methods. We demonstrate how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model. Finally, we demonstrate how ITrees can be executed using the Isabelle code generator to support the animation of models.

We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), an open, compositional and extensible framework for the verification of cyber-physical systems. We extend a previous semantic approach with methods and techniques that increase its expressivity, proof automation, and scalability to the level of state-of-the-art deductive verification tools. Our contributions include a user-friendly specification language, a flexible hybrid store model, including vectors and matrices, and separation-logic-style rules for local reasoning with hybrid stores using a novel form of differentiation called framed Fréchet derivatives. The formalisation of correctness specifications with forward predicate transformers, the certification of flows as unique solutions to systems of ordinary differential equations, and invariant reasoning for such systems also contribute to the scalability and usability of our framework. In combination, these features make our framework flexible and adaptable to several verification workflows. A suite of examples and hybrid systems verification benchmarks validate our framework relative to other state-of-the-art approaches.

RoboChart is a core notation in the RoboStar framework. It is a timed and probabilistic domain-specific and state machine-based language for robotics. RoboChart supports shared variables and communication across entities in its component model. It has formal denotational semantics given in CSP. The semantic technique of Interaction Trees (ITrees) represents behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisation of ITrees, ITree-based CSP semantics and a Z mathematical toolkit in Isabelle/HOL bring new applications of verification and animation for state-rich process languages, such as RoboChart. In this paper, we use ITrees to give RoboChart novel operational semantics, implement it in Isabelle, and use Isabelle's code generator to generate verified and executable animations. We illustrate our approach using an autonomous chemical detector and patrol robot models, exhibiting nondeterminism and using shared variables. With animation, we show two concrete scenarios for the chemical detector when the robot encounters different environmental inputs and three for the patrol robot when its calibrated position is in other corridor sections. We also verify that the animated scenarios are trace refinements of the CSP denotational semantics of the RoboChart models using FDR, a refinement model checker for CSP. This ensures that our approach to resolve nondeterminism using CSP operators with priority is sound and correct.

Assurance cases are used to communicate and assess confidence in critical system properties such as safety and security. Historically, assurance cases have been manually created documents, which are evaluated by system stakeholders through lengthy and complicated processes. In recent years, model-based system assurance approaches have gained popularity to improve the efficiency and quality of system assurance activities. This becomes increasingly important, as systems becomes more complex, it is a challenge to manage their development life-cycles, including coordination of development, verification and validation activities, and change impact analysis in inter-connected system assurance artifacts. Moreover, there is a need for assurance cases that support evolution during the operational life of the system, to enable continuous assurance in the face of an uncertain environment, as Robotics and Autonomous Systems (RAS) are adopted into society. In this paper, we contribute ACCESS - Assurance Case Centric Engineering of Safety-critical Systems, an engineering methodology, together with its tool support, for the development of safety critical systems around evolving model-based assurance cases. We show how model-based system assurance cases can trace to heterogeneous engineering artifacts (e.g. system architectural models, system safety analysis, system behaviour models, etc.), and how formal methods can be integrated during the development process. We demonstrate how assurance cases can be automatically evaluated both at development and runtime. We apply our approach to a case study based on an Autonomous Underwater Vehicle (AUV).

Assurance cases are used to communicate and assess confidence in critical system properties, e.g., safety and security. Historically, assurance cases have been manually created documents, validated by engineers through lengthy and error-prone processes. Recently, system assurance practitioners have begun adopting model-based approaches to improve the efficiency and quality of system assurance activities. This becomes increasingly important, for example, to ensure the safety of robotics and autonomous systems (RASs), as they are adopted into society. Such systems can be highly complex, and so it is a challenge to manage the development life-cycle and improve efficiency, including coordination of validation activities, and change impact analysis in interconnected system assurance artifacts. However, adopting model-based approaches require skills in the model management languages, which system assurance practitioners may not be acquainted with. In this article, we contribute an automated validation framework for the model-based assurance cases, which promotes the usage of a constrained natural language (CNL), that can be automatically transformed and executed against engineering models involved in assurance case development. We apply our approach to a case study based on an autonomous underwater vehicle (AUV).

Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic programs are ubiquitous, including having a significant 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 attracted much interest. Many challenges, however, remain. The work presented in this paper, probabilistic unifying relations (ProbURel), takes a step towards our vision to tackle these challenges. Our work is based on Hehner's predicative probabilistic programming, but there are several obstacles to the broader 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 Kleene's fixed-point theorem; (4) the enrichment of its semantics from distributions to subdistributions and superdistributions to deal with the constructive semantics; (5) the unique fixed-point theorem to 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 our work with six examples, including problems in robot localisation, classification in machine learning, and the termination of probabilistic loops. • A probabilistic semantics unification framework (ProbURel). • A new probabilistic programming language modelling Bayesian learning. • Iteration-based fix-point theorems and unique fix-point theorem for loops. • Mechanised theories in Isabelle/HOL and proved six examples.

Formal verification of cyber-physical systems requires that we can accurately model physical quantities. SI units allow a higher degree of rigour, since we can ensure compatibility of quantities in calculations. In this paper, we contribute a mechanisation of the International System of Quantities (ISQ) and the SI unit system in Isabelle/HOL. We show how Isabelle can be used to provide a type system for physical quantities, and automated proof support. Quantities are parameterised by dimension types and so only quantities of the same dimension can be equated. Our construction is validated by a test-set of known equivalences between both quantities and SI units. Moreover, the presented theory can be used for type-safe conversions between the SI system and others, like the British Imperial System (BIS).

RoboChart is a graphical language for model-based engineering of robotic systems, in the style of UML and SysML. It contains notations for data structures, system architecture, and the behaviour of individual robotic controllers using state machines. Crucially, RoboChart has a formal semantics in the CSP process algebra, which provides a precise foundation for software engineering and formal verification using model checking. However, due to state explosion, the application of model checking does not scale. In this paper, we contribute a compositional verification technique that uses Isabelle/HOL RoboChart state machines symbolically. Our technique uses state invariants to capture safety requirements over a very large or infinite state, similar to the B method, and is highly automated using Isabelle’s sledgehammer tool. We give a model transformation from the RoboTool development environment to Isabelle/HOL and apply this to several verification case studies.

Assurance cases (ACs) are an established practice for arguing confidence in critical system properties such as safety and security in high-risk industries.ACs use system artifacts to argue the aforementioned properties.Due to the iterative nature of system development, we need to update ACs to maintain assurance validity as a system evolves.For example, a changed design or an added hazard would result in re-evaluation of claims or a new claim to be verified.Thus, the generation and maintenance of ACs is a labour-intensive process.With the growing application of Model-based Engineering (MBE) in system development, it is beneficial to generate ACs from design models because this captures traceability, and enables automatic AC creation and update driven by model modification.Accordingly, the contribution of this paper is an automatic approach to AC generation and assembly from both unstructured design artifacts and UML-like design models within Eclipse.This approach also supports AC evidence generation by formal verification facilitated by automatically generated assertions.The realization of AC assembly and verification is supported by model query and model transformation.We apply our approach to an autonomous underwater robot with the RoboChart robotics modelling language.

Abstract RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.

Simulation and formal verification are important complementary techniques necessary in high assurance model-based systems development. In order to support coherent results, it is necessary to provide unifying semantics and automation for both activities. In this paper we apply Interaction Trees in Isabelle/HOL to produce a verification and simulation framework for state-rich process languages. We develop the core theory and verification techniques for Interaction Trees, use them to give a semantics to the CSP and Circus languages, and formally link our new semantics with the failures-divergences semantic model. We also show how the Isabelle code generator can be used to generate verified executable simulations for reactive and concurrent programs.

Abstract Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence, and overcome errant reasoning. However, assurance cases can never be fully formalised, as the use of formal methods is contingent on models that are validated by informal processes. Consequently, assurance techniques should support both formal and informal artifacts, with explicated inferential links between them. In this paper, we contribute a formal machine-checked interactive language, called Isabelle/SACM, supporting the computer-assisted construction of assurance cases compliant with the OMG Structured Assurance Case Meta-Model. The use of Isabelle/SACM guarantees well-formedness, consistency, and traceability of assurance cases, and allows a tight integration of formal and informal evidence of various provenance. In particular, Isabelle brings a diverse range of automated verification techniques that can provide evidence. To validate our approach, we present a substantial case study based on the Tokeneer secure entry system benchmark. We embed its functional specification into Isabelle, verify its security requirements, and form a modular security case in Isabelle/SACM that combines the heterogeneous artifacts. We thus show that Isabelle is a suitable platform for critical systems assurance.

The use of autonomous vehicles in real-world applications is often precluded by the difficulty of providing safety guarantees for their complex controllers. The simulation-based testing of these controllers cannot deliver sufficient safety guarantees, and the use of formal verification is very challenging due to the hybrid nature of the autonomous vehicles. Our work-in-progress paper introduces a formal verification approach that addresses this challenge by integrating the numerical computation of such a system (in GNU/Octave) with its hybrid system verification by means of a proof assistant (Isabelle). To show the effectiveness of our approach, we use it to verify differential invariants of an Autonomous Marine Vehicle with a controller switching between multiple modes.