arXiv subjects

James Baxter

Publications and source records attributed to James Baxter.

5 recordsLinked to original sources

arXiv2026

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.

cs.SE↗

arXiv2023

Understanding the leading indicators of hospital admissions from COVID-19 across successive waves in the UK

Following the UK Government's Living with COVID-19 Strategy and the end of universal testing, hospital admissions are an increasingly important measure of COVID-19 pandemic pressure. Understanding leading indicators of admissions at National Health Service (NHS) Trust, regional and national geographies help health services plan capacity needs and prepare for ongoing pressures. We explored the spatio-temporal relationships of leading indicators of hospital pressure across successive waves of SARS-CoV-2 incidence in England. This includes an analysis of internet search volume values from Google Trends, NHS triage calls and online queries, the NHS COVID-19 App, lateral flow devices and the ZOE App. Data sources were analysed for their feasibility as leading indicators using linear and non-linear methods; granger causality, cross correlations and dynamic time warping at fine spatial scales. Consistent temporal and spatial relationships were found for some of the leading indicators assessed across resurgent waves of COVID-19. Google Trends and NHS queries consistently led admissions in over 70% of Trusts, with lead times ranging from 5-20 days, whereas an inconsistent relationship was found for the ZOE app, NHS COVID-19 App, and rapid testing, that diminished with granularity, showing limited autocorrelation of leads between -7 to 7 days. This work shows that novel syndromic surveillance data has utility for understanding the expected hospital burden at fine spatial scales. The analysis shows at low level geographies that some surveillance sources can predict hospital admissions, though care must be taken in relying on the lead times and consistency between waves.

stat.AP↗

arXiv2019

Priorities in tock-CSP

The $tock$-CSP encoding embeds a rich and flexible approach to modelling discrete timed behaviours in CSP where the event $tock$ is interpreted to mark the passage of time. The model checker FDR provides tailored support for $tock$-CSP, including a prioritisation operator that has typically been used to ensure maximal progress, where time only advances after internal activity has stabilised. Prioritisation may also be used on its own right as a modelling construct. Its operational semantics, however, is only congruent over the most discriminating semantic model of CSP: the finite-linear model. To enable sound and compositional reasoning in a $tock$-CSP setting, we calculate a denotational definition for prioritisation. For that we establish a Galois connection between a specialisation of the finite-linear model, with $tock$ and $\checkmark$, that signals termination, as special events, and $\checkmark$-$tock$-CSP, a model for $tock$-CSP that captures termination, deadlines, and is adequate for reasoning about timed refinement. Our results are mechanised using Isabelle/HOL.

cs.LO↗

arXiv2019

Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP

The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He's Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantic models. These can be further applied in the development of verification tools, harnessing Isabelle's proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, including algebraic and axiomatic semantics, proof tools for Hoare logic and refinement calculus, and UTP theories to encode computational paradigms.

cs.LO↗

arXiv2018

Automating Verification of State Machines with Reactive Designs and Isabelle/UTP

State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if they are both automated and scalable. In this paper, we present a verification approach for a diagrammatic state machine language that utilises theorem proving and a denotational semantics based on Unifying Theories of Programming (UTP). We provide the necessary theory to underpin state machines (including induction theorems for iterative processes), mechanise an action language for states and transitions, and use these to formalise the semantics. We then describe the verification approach, which supports infinite state systems, and exemplify it with a fully automated deadlock-freedom check. The work has been mechanised in our proof tool, Isabelle/UTP, and so also illustrates the use of UTP to build practical verification tools.

cs.LO↗