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.

Abstract It is often the case that a robot must adapt to unexpected changes in its environment. It is, however, important that these changes can be demonstrated to maintain the safe operation of the robot. The adaptive systems community has developed the MAPE-K pattern as a widely recognised conceptual architecture. We propose extending MAPE-K to incorporate runtime verification, resulting in an architecture we call MAPLE-K. In this paper, we capture and formalise both the MAPE-K and MAPLE-K architectures using a domain-specific language. Additionally, we provide support for translation from architectural models to software models and code to facilitate the deployment of verified applications. MAPE-K is rarely maintained at the implementation level, but our work ensures traceability between the code and its design, enabling the use of architectural information to verify the correctness of the software.

Simulation is a favoured technique in robotics. It is, however, costly, in terms of development time, and its usability is limited by the lack of standardisation and portability of simulators. We present RoboSim, a diagrammatic tool-independent domain-specific language to model robotic platforms and their controllers. It can be regarded as a profile of UML/SysML enriched with time primitives, differential equations, and a mathematical semantics. Our previous work on RoboSim described a notation to specify control software. In this paper, we present a novel notation to describe physical models: block diagrams that can be linked to the platform-independent software model to characterise how services required by the software are realised by actuators and sensors. Behaviours are specified by differential equations, and simulations and mathematical models of the whole system can be generated automatically. Our main contributions are a modular and extensible diagrammatic notation that supports the explicit specification of physical behaviours; a set of validation rules that identify well-formed models; a model-to-model transformation from RoboSim to an input format accepted by several simulators; and a formal semantics for mathematical reasoning.

A robot affects and is affected by its environment, so that typically its behaviour depends on properties of that environment. For verification, we need to formalise those properties. Modelling the environment is very challenging, if not impossible, but we can capture assumptions. Here, we present RoboWorld, a domain-specific controlled natural language with a process algebraic semantics that can be used to define (a) operational requirements, and (b) environment interactions of a robot. RoboWorld is part of the RoboStar framework for verification of robotic systems. In this article, we define RoboWorld’s syntax and hybrid semantics, and illustrate its use for capturing operational requirements, for automatic test generation, and for proof. We also present a tool that supports the writing of RoboWorld documents. Since RoboWorld is a controlled natural language, it complements the other RoboStar notations in being accessible to roboticists, while at the same time benefitting from a formal semantics to support rigorous verification (via testing and proof).

The existing testing theories for CSP cater for verification of interaction patterns (traces) and deadlocks, but not time. We address here refinement and testing based on a dialect of CSP, called tock -CSP, which can capture discrete time properties. This version of CSP has been of widespread interest for decades; recently, it has been given a denotational semantics, and model checking has become possible using a well established tool. Here, we first equip tock -CSP with a novel semantics for testing, which distinguishes input and output events: the standard models of ( tock -)CSP do not differentiate them, but for testing this is essential. We then present a new testing theory for timewise refinement, based on novel definitions of test and test execution. Finally, we reconcile refinement and testing by relating timed ioco testing and refinement in tock -CSP with inputs and outputs. With these results, this paper provides, for the first time, a systematic theory that allows both timed testing and timed refinement to be expressed. An important practical consequence is that this ensures that the notion of correctness used by developers guarantees that tests pass when applied to a correct system and, in addition, faults identified during testing correspond to development mistakes.

Abstract Specifying budgets and deadlines using a process algebra like CSP requires an explicit notion of time. The tock-CSP encoding embeds a rich and flexible approach for modelling discrete-time behaviours with powerful tool support. It uses an event tock, interpreted to mark passage of time. Analysis, however, has traditionally used the standard semantics of CSP, which is inadequate for reasoning about timed refinement. The most recent version of the model checker FDR provides tailored support for tock-CSP, including specific operators, but the standard semantics remains inadequate. In this paper, we characterise tock-CSP as a language in its own right, rich enough to model budgets and deadlines, and reason about Zeno behaviour. We present the first sound tailored semantic model for tock-CSP that captures timewise refinement. It is fully mechanised in Isabelle/HOL and, to enable use of FDR4 to check refinement in this novel model, we use model shifting, which is a technique that explicitly encodes refusals in traces.

Safety-Critical Java (SCJ) is a version of Java suitable for programming real-time safety-critical systems; it is the result of an international standardisation effort to define a subset of the Real-Time Specification for Java (RTSJ). SCJ programs require the use of specialised virtual machines. We present here the result of our verification of the scheduler of the only SCJ virtual machine up to date with the standard and publicly available, the icecap HVM. We describe our approach for analysis of (SCJ) virtual machines, and illustrate it using the icecap HVM scheduler. Our work is based on a state-rich process algebra that combines Z and CSP, and we take advantage of well established tools.