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.

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 a formal denotational semantics given in CSP. Interaction Trees (ITrees) is a semantic technique to represent behaviours of reactive and concurrent programs interacting with their environments. Recent mechanisations of ITrees along with 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 a 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 model. With animation, we show two concrete scenarios when the robot encounters different environmental inputs.

Semantics for nondeterministic probabilistic sequential programs has been well studied in the past decades. In a variety of semantic models, how nondeterministic choice interacts with probabilistic choice is the most significant difference. In He, Morgan, and McIver’s relational model, probabilistic choice refines nondeterministic choice. This model is general because of its predicative-style semantics in Hoare and He’s Unifying Theories of Programming, and suitable for automated reasoning because of its algebraic feature. Previously, we gave probabilistic semantics to the RoboChart notation based on this model, and also formalised the proof that the semantic embedding is a homomorphism, and revealed interesting details. In this paper, we present our mechanisation of the proof in Isabelle/UTP enabling automated reasoning for probabilistic sequential programs including a subset of the RoboChart language. With mechanisation, we even reveal more interesting questions, hidden in the original model. We demonstrate several examples, including an example to illustrate the interaction between nondeterministic choice and probabilistic choice, and a RoboChart model for randomisation based on binary probabilistic choice.

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.

Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infinite state space. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program’s denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, based on Kleene algebra, and for parallel composition. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He’s Unifying Theories of Programming (UTP) framework, to provide soundness guarantees and practical verification support.

Simulink is widely accepted in industry for model-based designs. Verification of Simulink diagrams against contracts or implementations has attracted the attention of many researchers. We present a compositional assume-guarantee reasoning framework to provide a purely relational mathematical semantics for discrete-time Simulink diagrams, and then to verify the diagrams against the contracts in the same semantics in UTP. We define semantics for individual blocks and composition operators, and develop a set of calculation laws (based on the equational theory) to facilitate automated proof. An industrial safety-critical model is verified using our approach. Furthermore, all these definitions, laws, and verification of the case study are mechanised in Isabelle/UTP, an implementation of UTP in Isabelle/HOL.

Reactive programs are ubiquitous in modern applications, and so verification is highly desirable. We present a verification strategy for reactive programs with a large or infinite state space utilising algebraic laws for reactive relations. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program’s denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, which is supported by Kleene algebra. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, which provides soundness guarantees, and practical verification support.

Since state-rich formalism is a combination of Z, CSP, refinement calculus and Dijkstra’s guarded commands, its model checking is intrinsically more complicated and difficult than that of individual state-based languages or process algebras. Current solutions translate executable constructs of programs to Java with JCSP, or translate them to CSP processes. Data aspects of programs are expressed in the Java programming language or as CSP processes. Both of them have disadvantages. This work presents a new approach to model-checking by linking it to $$CSP ∥ B$$CSP‖B; then we utilise ProB to model-check and animate the $$CSP ∥ B$$CSP‖B program. The most significant advantage of this approach is the direct mapping of the state part in to Z and finally to B, which maintains the high-level abstraction of data specification. In addition, introduction of deadlock, invariant violation checking, LTL formula checking and animation is another key advantage. We present our approach, a link definition for a subset of constructs, as well as a popular case study (reactive buffer) to show the practical usability of our work. We conclude with a discussion of related work, advantages and potential limitations of our approach and future work.