Continuous dynamical systems are fundamental in modelling a wide range of real-world phenomena, from cyber-physical systems to industrial automation. Such systems operate in dynamic environments where unanticipated situations can arise. Requirements specified at design time may become partially unachievable when the system is deployed. We propose a novel method for reachability specification degradation tailored to continuous dynamical systems. Our approach involves sampling points within the initial state space region, estimating reachability regions over time using the Lipschitz constant, and augmenting the original specification through disjunction operations. We implement our method to support how a system can adapt to requirements in real time.

Formal verification is crucial for ensuring the robustness of security protocols against adversarial attacks. The Needham-Schroeder protocol, a foundational authentication mechanism, has been extensively studied, including its integration with Physical Layer Security (PLS) techniques such as watermarking and jamming. Recent research has used ProVerif to verify these mechanisms in terms of secrecy. However, the ProVerif-based approach limits the ability to improve understanding of security beyond verification results. To overcome these limitations, we re-model the same protocol using an Isabelle formalism that generates sound animation, enabling interactive and automated formal verification of security protocols. Our modelling and verification framework is generic and highly configurable, supporting both cryptography and PLS. For the same protocol, we have conducted a comprehensive analysis (secrecy and authenticity in four different eavesdropper locations under both passive and active attacks) using our new web interface. Our findings not only successfully reproduce and reinforce previous results on secrecy but also reveal an uncommon but expected outcome: authenticity is preserved across all examined scenarios, even in cases where secrecy is compromised. We have proposed a PLS-based Diffie-Hellman protocol that integrates watermarking and jamming, and our analysis shows that it is secure for deriving a session key with required authentication. These highlight the advantages of our novel approach, demonstrating its robustness in formally verifying security properties beyond conventional methods.

RoboChart is a core notation in the RoboStar framework which brings modern modelling and formal verification technologies into software engineering for robotics. It is a timed and probabilistic domain-specific language for robotics and provides a UML-like architectural and state machine modelling. This work presents RoboCertProb for specifying quantitative properties of probabilistic robotic systems modelled in RoboChart. RoboCertProb's semantics is based on PCTL*. To interpret RoboCertProb over RoboChart models, we give a Markov semantics (DTMCs and MDPs) to RoboChart, derived from its existing transformation semantics to the PRISM language. In addition to property specification, RoboCertProb also entitles us to configure loose constants and unspecified functions and operations in RoboChart models. It allows us to set up environmental inputs to verify reactive probabilistic systems not directly supported in probabilistic model checkers like PRISM because they employ a closed-world assumption. We implement RoboCertProb in an accompanying tool of RoboChart, RoboTool, for specifying properties and automatically generating PRISM properties from them to formally verify RoboChart models using PRISM. We have used it to analyse the behaviour of software controllers for two real robots: an industrial painting robot and an agricultural robot for treating plants with UV lights.

Probabilistic model checking is a widely used formal verification technique to automatically verify qualitative and quantitative properties for probabilistic models. However, capturing such systems, writing corresponding properties, and verifying them require domain knowledge. This makes it not accessible for researchers and engineers who may not have the required knowledge. Previous studies have extended UML activity diagrams (ADs), developed transformations, and implemented accompanying tools for automation. The research, however, is incomprehensive and not fully open, which makes it hard to be evaluated, extended, adapted, and accessed. In this paper, we propose a comprehensive verification framework for ADs, including a new profile for probability, time, and quality annotations, a semantics interpretation of ADs in three Markov models, and a set of transformation rules from activity diagrams to the PRISM language, supported by PRISM and Storm. Most importantly, we developed algorithms for transformation and implemented them in a tool, called QASCAD, using model-based techniques, for fully automated verification. We evaluated one case study where multiple robots are used for delivery in a hospital and further evaluated six other examples from the literature. With all these together, this work makes noteworthy contributions to the verification of ADs by improving evaluation, extensibility, adaptability, and accessibility.

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.

Continued adoption of agricultural robots postulates the farmer's trust in the reliability, robustness and safety of the new technology. This motivates our work on safety assurance of agricultural robots, particularly their ability to detect, track and avoid obstacles and humans. This paper considers a probabilistic modelling and risk analysis framework for use in the early development phases. Starting off with hazard identification and a risk assessment matrix, the behaviour of the mobile robot platform, sensor and perception system, and any humans present are captured using three state machines. An auto-generated probabilistic model is then solved and analysed using the probabilistic model checker PRISM. The result provides unique insight into fundamental development and engineering aspects by quantifying the effect of the risk mitigation actions and risk reduction associated with distinct design concepts. These include implications of adopting a higher performance and more expensive Object Detection System or opting for a more elaborate warning system to increase human awareness. Although this paper mainly focuses on the initial concept-development phase, the proposed safety-assurance framework can also be used during implementation, and subsequent deployment and operation phases.

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.

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.

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.

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.

We outline a probabilistic denotational semantics for the RoboChart language, a diagrammatic, domain-specific notation for describing robotic controllers with their hardware platforms and operating environments. We do this using a powerful (but perhaps not so well known) semantic technique: He, Morgan, and McIver’s weakest completion semantics, which is based on Hoare and He’s Unifying Theories of Programming. In this approach, we do the following: (1) start with the standard semantics for a nondeterministic programming language; (2) propose a new probabilistic semantic domain; (3) propose a forgetful function from the probabilistic semantic domain to the standard semantic domain; (4) use the converse of the forgetful function to embed the standard semantic domain in the probabilistic semantic domain; (5) demonstrate that this embedding preserves program structure; (6) define the probabilistic choice operator. Weakest completion semantics guides the semantic definition of new languages by building on existing semantics and, in this case, tackling a notoriously thorny issue: the relationship between demonic and probabilistic choice. Consistency ensures that programming intuitions, development techniques, and proof methods can be carried over from the standard language to the probabilistic one. We largely follow He et al., our contribution being an explication of the technique with meticulous proofs suitable for mechanisation in Isabelle/UTP.

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 [Figure not available: see fulltext.] 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 [Figure not available: see fulltext.] programs to Java with JCSP, or translate them to CSP processes. Data aspects of [Figure not available: see fulltext.] 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 [Figure not available: see fulltext.] by linking it to $$CSP \parallel B$$CSPźB; then we utilise ProB to model-check and animate the $$CSP \parallel B$$CSPźB program. The most significant advantage of this approach is the direct mapping of the state part in [Figure not available: see fulltext.] 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 [Figure not available: see fulltext.] 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.

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 ; then we utilise ProB to model-check and animate the 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.

Computer-based systems are becoming more and more complex. It is really a grand challenge to assure the dependability of these systems with the growing complexity, especially for high integrity and safety critical systems that require extremely high dependability. Circus, as a formal language, is designed to tackle this problem by providing precision preservation and correctness assurance. It is a combination of Z, CSP, refinement calculus and Dijkstra's guarded commands. A main objective of Circus is to provide calculational style refinement that differentiates itself from other integrated formal methods. Looseness, which is introduced from constants and uninitialised state space in Circus, and nondeterminism, which is introduced from disjunctive operations and CSP operators, make model checking of Circus more difficult than that of sole CSP or Z. Current approaches have a number of disadvantages like nondeterminism and divergence information loss, abstraction deterioration, and no appropriate tools to support automation. In this thesis, we present a new approach to model-check state-rich formalisms by linking them to a combination of a state-based formalism and a process algebra. Specifically, the approach illustrated in this thesis is to model-check Circus by linking to CSP || B. Eventually, we can use ProB, a model checker for B, Event-B, and CSP || B etc., to check the resultant CSP || B model. A formal link from Circus to CSP || B is defined in our work. Our link solution is to rewrite Circus models first to make all interactions between the state part and the behavioural part of Circus only through schema expressions, then translate the state part and the behavioural part to B and CSP respectively. In addition, since the semantics of Circus is based on Hoare and He's Unifying Theories of Programming (UTP), in order to prove the soundness of our link, we also give UTP semantics to CSP || B. Finally, because both ends of the link have their semantics defined in UTP, they are comparable. Furthermore, in order to support an automatic translation process, a translator is developed. It has supported almost all constructs defined in the link though with some limitations. Finally, three case studies are illustrated to show the usability of our model checking solution as well as limitations. The bounded reactive buffer is a typical Circus example. By our model checking approach, basic properties like deadlock freedom and divergence freedom for both the specification and the implementation with a small buffer size have been verified. In addition, the implementation has been verified to be a refinement of the specification in terms of traces and failures. Afterwards, in the Electronic Shelf Edge Label (ESEL) case study, we demonstrate how to use Circus to model different development stages of systems from the specification to two more specific systems. We have verified basic properties and sequential refinements of three models as well as three application related properties. Similarly, only the systems with a limited number of ESELs are verified. Finally, we present the steam boiler case study. It is a real and industrial control system problem. Though our solution cannot model check the steam boiler model completely due to its large state space, our solution still proves its benefits. Through our model checking approach, we have found a substantial number of errors from the original Circus solution. Then with counterexamples during animation and model checking, we have corrected all these found errors.