Publications (31)
Unifying Theories of Reactive Design Contracts
Simon Foster, Ana Cavalcanti, Samuel Canham +2
Design-by-contract is an important technique for model-based design in which a composite system is specified by a collection of contracts that specify the behavioural assumptions a…
Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
Simon Foster, James Baxter, Ana Cavalcanti +2
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 v…
Brownian Motion in Isabelle/HOL
Christian Pardillo Laursen, Simon Foster, Mark Post
In order to formally verify robotic controllers, we must tackle the inherent uncertainty of sensing and actuation in a physical environment. We can model uncertainty using stochast…
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher +1
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for…
Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
Simon Foster, Kangfeng Ye, Ana Cavalcanti +1
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…
ACCESS: Assurance Case Centric Engineering of Safety-critical Systems
Ran Wei, Simon Foster, Haitao Mei +7
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 do…