| Papers | Theses | Technical Reports |
@article{FosterHW2025,
author = {S.~Foster and C.-K.~Hur and J.~Woodcock},
title = {Unifying Model Execution and Deductive Verification
with Interaction Trees in {Isabelle/HOL}},
year = {2025},
issue_date = {May 2025},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {34},
number = {4},
issn = {1049-331X},
doi = {10.1145/3702981},
journal = {ACM Trans. Softw. Eng. Methodol.},
month = apr,
articleno = {108},
numpages = {40},
keywords = {Interaction Trees (ITrees), Isabelle/HOL, Model
Execution, Deductive Verification, Coinductive
Structures, Formal Methods, CSP (Communicating
Sequential Processes), Circus Language, Z and B
Methods, Structural Operational Semantics, Theorem
Proving, Proof Automation, Software Engineering
Models, Model Execution, High-Assurance Software,
Automated Program Verification, Code Generation,
Animation and Simulation, UTP (Unifying Theories of
Programming), Imperative Programming Verification}
}
@inproceedings{AdamAR2025,
title = {A Verification Methodology for Safety Assurance of
RAS},
author = {M.~Adam and D.~A.~Anisi and P.~Ribeiro},
booktitle = {Annual Conference Towards Autonomous Robotic
Systems},
pages = {281--294},
year = {2025},
organization = {Springer},
doi = {10.1007/978-3-032-01486-3_23}
}
@inproceedings{AttalaYFCW2025,
author = {Z.~Attala and F.~Yan and S.~Foster and A.~Cavalcanti and J.~Woodcock},
title = {Process-Algebraic Semantics for Verifying
Intelligent Robotic Control Software},
year = {2025},
isbn = {978-3-031-93705-7},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
doi = {10.1007/978-3-031-93706-4_2},
booktitle = {NASA Formal Methods: 17th International Symposium,
NFM 2025, Williamsburg, VA, USA, June 11–13, 2025,
Proceedings},
pages = {11–30},
numpages = {20},
keywords = {verification, Circus, theorem proving, Isabelle,
Marabou},
location = {Hampton Roads, VA, USA}
}
@inproceedings{BaxterAKWCG2025,
author = {J.~Baxter and B.~Van~Acker and M.~Kristensen and T.~Wright and A.~Cavalcanti and C.~Gomes},
title = {Formal Architectural Patterns for Adaptive Robotic
Software},
year = {2025},
isbn = {978-3-031-90899-6},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
doi = {10.1007/978-3-031-90900-9_8},
booktitle = {Fundamental Approaches to Software Engineering: 28th
International Conference, FASE 2025, Held as Part of
the International Joint Conferences on Theory and
Practice of Software, ETAPS 2025, Hamilton, ON,
Canada, May 3–8, 2025, Proceedings},
pages = {145–165},
numpages = {21},
keywords = {adaptive systems, robotics, formal modelling},
location = {Hamilton, ON, Canada}
}
@inproceedings{HendryCMC2025,
author = {H.~Hendry and A.~Cavalcanti and C.~McCall and M.~Chattington},
title = {{RoboScene}: Notation for Formal Verification of
Human-Robot Interaction},
year = {2025},
isbn = {978-3-031-90899-6},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
doi = {10.1007/978-3-031-90900-9_9},
booktitle = {Fundamental Approaches to Software Engineering: 28th
International Conference, FASE 2025, Held as Part of
the International Joint Conferences on Theory and
Practice of Software, ETAPS 2025, Hamilton, ON,
Canada, May 3–8, 2025, Proceedings},
pages = {166–187},
numpages = {22},
keywords = {RoboStar, Sequence diagrams, CSP, HCE},
location = {Hamilton, ON, Canada}
}
@article{MiyazawaACBPRTW2025,
author = {A.~Miyazawa and S.~Ahmadi and A.~Cavalcanti and J.~Baxter and M.~Post and P.~Ribeiro and J.~Timmis and T.~Wright},
title = {Diagrammatic physical robot models},
journal = {Software and Systems Modeling},
pages = {1--45},
year = {2025},
publisher = {Springer},
doi = {10.1007/s10270-025-01270-9}
}
This paper describes use of model checking to verify synchronisation properties of an industrial welding system consisting of a cobot arm and an external turntable. The robots must move synchronously, but sometimes get out of synchronisation, giving rise to unsatisfactory weld qualities in problem areas, such as around corners. These mistakes are costly, since time is lost both in the robotic welding and in manual repairs needed to improve the weld. Verification of the synchronisation properties has shown that they are fulfilled as long as assumptions of correctness made about parts outside the scope of the model hold, indicating limitations in the hardware. These results have indicated the source of the problem, and motivated a re-calibration of the real-life system. This has drastically improved the welding results, and is a demonstration of how formal methods can be useful in an industrial setting.
@article{MurrayNARC2024,
author = {Y.~Murray and H.~Nordlie and D.~A.~Anisi and P.~Ribeiro and A~Cavalcanti},
title = {Model Checking and Verification of Synchronisation
Properties of Cobot Welding},
note = {Publisher Copyright: {\textcopyright} Y. Murray, H.
Nordlie, D.A. Anisi, P. Ribeiro & A. Cavalcanti.;
6th International Workshop on Formal Methods for
Autonomous Systems, FMAS 2024 ; Conference date:
11-11-2024 Through 13-11-2024},
year = {2024},
month = nov,
day = {21},
doi = {10.4204/EPTCS.411.6},
language = {English},
volume = {411},
pages = {91--108},
journal = {Electronic Proceedings in Theoretical Computer
Science, EPTCS},
issn = {2075-2180},
publisher = {Open Publishing Association}
}
@inproceedings{AdamHAAC2024,
author = {M.~Adam and E.~E.~Hartmark and T.~Andersen and D.~A.~Anisi and A.~Cavalcanti},
title = {Safety assurance of autonomous agricultural robots:
from offline model-checking to runtime verification},
booktitle = {2024 IEEE 20th International Conference on
Automation Science and Engineering (CASE)},
year = {2024},
pages = {2511-2516},
doi = {10.1109/CASE59546.2024.10711810}
}
@article{LarsenABCGLMOPP2024,
author = {P.~G.~Larsen and S.~Ali and R.~Behrens and A.~Cavalcanti and C.~Gomes and G.~Li and Meulenaere, P.~De and M.~L.~Olsen and N.~Passalis and T.~Peyrucain and et al.},
title = {Robotic safe adaptation in unprecedented situations:
the RoboSAPIENS project},
volume = {2},
doi = {10.1017/cbp.2024.4},
journal = {Research Directions: Cyber-Physical Systems},
year = {2024},
pages = {e4}
}
We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), an open, compositional and extensible framework for the verification of cyber-physical systems. We extend a previous semantic approach with methods and techniques that increase its expressivity, proof automation, and scalability to the level of state-of-the-art deductive verification tools. Our contributions include a user-friendly specification language, a flexible hybrid store model, including vectors and matrices, and separation-logic-style rules for local reasoning with hybrid stores using a novel form of differentiation called framed Fréchet derivatives. The formalisation of correctness specifications with forward predicate transformers, the certification of flows as unique solutions to systems of ordinary differential equations, and invariant reasoning for such systems also contribute to the scalability and usability of our framework. In combination, these features make our framework flexible and adaptable to several verification workflows. A suite of examples and hybrid systems verification benchmarks validate our framework relative to other state-of-the-art approaches.
@article{HuertayMuniveFGSPH2024,
author = {J.~J.~Huerta~y~Munive and S.~Foster and M.~Gleirscher and G.~Struth and C.~Pardillo~Laursen and T.~Hickman},
title = {IsaVODEs: Interactive Verification of Cyber-Physical
Systems at Scale},
journal = {Journal of Automated Reasoning},
year = {2024},
volume = {68},
number = {4},
pages = {21},
issn = {1573-0670},
doi = {10.1007/s10817-024-09709-2},
url = {https://doi.org/10.1007/s10817-024-09709-2}
}
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.
@article{YeWF24,
author = {K.~Ye and J.~Woodcock and S.~Foster},
title = {Probabilistic unifying relations for modelling
epistemic and aleatoric uncertainty: Semantics and
automated reasoning with theorem proving},
journal = {Theoretical Computer Science},
volume = {1021},
pages = {114876},
year = {2024},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2024.114876},
url = {https://www.sciencedirect.com/science/article/pii/S0304397524004936},
keywords = {Formal semantics, Fixed-point theorems, Predicative
programming, UTP, Probabilistic models,
Probabilistic programs, Probability distributions,
Formal verification, Quantitative verification,
Automated reasoning, Theorem proving, Isabelle/HOL,
Robotics, Machine learning, Classification}
}
Although digital twins have been around for decades, there are many areas of research that need to be pursued in order to enable trustworthy predictions. The existing challenges and the future directions to take can be organised in many different ways. In this chapter, the foundational issues that we still think require clarification comes first. This is followed by research challenges in the different platforms needed to be able to produce digital twins in a cost-efficient manner. Afterwards the research changes for enabling autonomy of digital twins (uncertainty in many areas may hinder an accurate estimation of the state). Finally, research in composition of digital twins is considered and this really goes into system of systems considerations where an eco-system of stakeholders needs to agree about the means of composition.
@inbook{LarsenFGWBUERHO24,
author = {P.~G.~Larsen and J.~Fitzgerald and C.~Gomes and J.~Woodcock and S.~Basagiannis and A.~Ulisse and L.~Esterle and D.~E.~L.~R{\"o}tter and S.~T.~Hansen and B.~J.~Oakes},
editor = {Fitzgerald, John and Gomes, Cl{\'a}udio and Larsen, Peter Gorm},
title = {Future Directions and Challenges},
booktitle = {The Engineering of Digital Twins},
year = {2024},
publisher = {Springer International Publishing},
address = {Cham},
pages = {363--386},
isbn = {978-3-031-66719-0},
doi = {10.1007/978-3-031-66719-0_15},
url = {https://doi.org/10.1007/978-3-031-66719-0_15}
}
As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this difficult task, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues, such as conflicts, redundancy, restrictiveness, and insufficiency, yielding diagnostics that pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs, comprising 62 issues for the software underpinning the operation of systems, such as, assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.
@inproceedings{FengMYBAMTSSIRCCC24,
author = {N.~Feng and L.~Marsso and S.~G.~Yaman and Y.~Baatartogtokh and R.~Ayad and V.~O.~D.~Mello and B.~Townsend and I.~Standen and I.~Stefanakos and C.~Imrie and G.~N.~Rodrigues and A.~L.~C.~Cavalcanti and R.~Calinescu and M.~Chechik},
title = {Analyzing and Debugging Normative Requirements via
Satisfiability Checking},
year = {2024},
isbn = {9798400702174},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3597503.3639093},
doi = {10.1145/3597503.3639093},
booktitle = {Proceedings of the IEEE/ACM 46th International
Conference on Software Engineering},
articleno = {214},
numpages = {12},
location = {Lisbon, Portugal},
series = {ICSE '24}
}
A growing range of applications use AI and other autonomous agents to perform tasks that raise social, legal, ethical, empathetic, and cultural (SLEEC) concerns. To support a framework for the consideration of these concerns, we introduce SLEEC-TK, a toolkit for specification, validation, and verification of SLEEC requirements. SLEEC-TK is an Eclipse-based environment for defining SLEEC rules in a domain-specific language with a timed process algebraic semantics. SLEEC-TK uses model checking to identify redundant and conflicting rules, and to verify conformance of design models with SLEEC rules. We illustrate the use of SLEEC-TK for an assistive-care robot.
@article{YamanRBJCC24,
author = {S.~G.~Yaman and P.~Ribeiro and C.~Burholt and M.~Jones and A.~L.~C.~Cavalcanti and R.~Calinescu},
title = {Toolkit for specification, validation and
verification of social, legal, ethical, empathetic
and cultural requirements for autonomous agents},
journal = {Science of Computer Programming},
volume = {236},
pages = {103118},
year = {2024},
issn = {0167-6423},
doi = {https://doi.org/10.1016/j.scico.2024.103118},
url = {https://www.sciencedirect.com/science/article/pii/S0167642324000418},
keywords = {Autonomous agents, Social, legal, ethical,
empathethic and cultural requirements, Verification
and validation}
}
Current practice in simulation and implementation of robot controllers is usually undertaken with guidance from high-level design diagrams and pseudocode. Thus, no rigorous connection between the design and the development of a robot controller is established. This paper presents a framework for designing robotic controllers with support for automatic generation of executable code and automatic property checking. A state-machine based notation, RoboChart, and a tool (RoboTool) that implements the automatic generation of code and mathematical models from the designed controllers are presented. We demonstrate the application of RoboChart and its related tool through a case study of a robot performing an exploration task. The automatically generated code is platform independent and is used in both simulation and two different physical robotic platforms. Properties are formally checked against the mathematical models generated by RoboTool, and further validated in the actual simulations and physical experiments. The tool not only provides engineers with a way of designing robotic controllers formally but also paves the way for correct implementation of robotic systems.
@article{LiRMRCAWT24,
author = {W.~Li and P.~Ribeiro and A.~Miyazawa and R.~Redpath and A.~Cavalcanti and K.~Alden and J.~Woodcock and J.~Timmis},
title = {Formal design, verification and implementation of
robotic controller software via RoboChart and
RoboTool},
journal = {Autonomous Robots},
volume = {48},
number = {6},
pages = {14},
year = {2024},
publisher = {Springer}
}
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.
@article{YeFW24,
author = {K.~Ye and S.~Foster and J.~Woodcock},
title = {Formally verified animation for RoboChart using
interaction trees},
journal = {Journal of Logical and Algebraic Methods in
Programming},
volume = {137},
pages = {100940},
year = {2024},
issn = {2352-2208},
doi = {10.1016/j.jlamp.2023.100940},
url = {https://www.sciencedirect.com/science/article/pii/S2352220823000949},
keywords = {Interaction trees, CSP, Operational semantics,
Animation of robot software, Theorem proving, Code
generation}
}
State machines are widely used in industry and academia to capture behavioural models of control. They are included in popular notations, such as UML and its variants, and used (sometimes informally) to describe computational artefacts. In this paper, we present laws for state machines that we prove sound with respect to a process algebraic semantics for refinement, and complete, in that they are sufficient to reduce an arbitrary model to a normal form that isolates basic (action and control) elements. We consider two variants of UML-like state machines, both enriched with facilities to deal with time budgets, timeouts and deadlines over triggers and actions. In the first variant, machines are self-contained components, declaring all the variables, events and operations that they require or define. In contrast, in the second variant, machines are open, like in UML for instance. Laws for open state machines do not depend on a specific context of variables, events and operations, and normalization uses a novel operator for open-machine (de)composition. Our laws can be used in behaviour-preservation transformation techniques. Their applications are automated by a model-transformation engine.
@article{CavalcantiFRS23,
author = {A.~Cavalcanti and M.~C.~Filho and P.~Ribeiro and A.~Sampaio},
title = {Laws of Timed State Machines},
journal = {The Computer Journal},
pages = {bxad124},
year = {2023},
month = dec,
issn = {0010-4620},
doi = {10.1093/comjnl/bxad124},
url = {https://academic.oup.com/comjnl/advance-article-pdf/doi/10.1093/comjnl/bxad124/55978269/bxad124.pdf}
}
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).
@article{BaxterCCJ23,
author = {J.~Baxter and G.~Carvalho and A.~Cavalcanti and F.~R.~J\'{u}nior},
title = {{RoboWorld}: Verification of Robotic Systems with
Environment in the Loop},
year = {2023},
issue_date = {December 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {35},
number = {4},
issn = {0934-5043},
url = {https://doi.org/10.1145/3625563},
doi = {10.1145/3625563},
journal = {Form. Asp. Comput.},
month = nov,
articleno = {26},
numpages = {46},
keywords = {hybrid systems, Model-driven engineering,
domain-specific languages, process algebra,
controlled natural languages}
}
@inproceedings{SantosFS2023,
author = {M.~Santos and M.~C.~Filho and A.~Sampaio},
booktitle = {2023 Latin American Robotics Symposium (LARS), 2023
Brazilian Symposium on Robotics (SBR), and 2023
Workshop on Robotics in Education (WRE)},
title = {A Model-based Approach to the Development and
Verification of Robotic Systems for Competitions},
year = {2023},
pages = {236-241},
keywords = {Systematics;Navigation;Education;Model
checking;Autonomous aerial vehicles;Control
systems;Indoor environment},
doi = {10.1109/LARS/SBR/WRE59448.2023.10333030}
}
Verifying learning robotic systems is challenging. Existing techniques and tools for verification of an artificial neural network (ANN) are concerned with component-level properties. Here, we deal with robotic systems whose control software uses ANN components, and with properties of that software that may depend on all components. Our focus is on trained fully connected ReLU neural networks for control. We present an approach to (1) modelling ANN components as part of behavioural models for control software and (2) verification using traditional and ANN-specific verification tools. We describe our results in the context of RoboChart, a domain-specific modelling language for robotics with support for formal verification. We describe our modelling notation and a strategy for automated proof using Isabelle and Marabou, for example.
@inproceedings{AttalaCW23,
author = {Z.~Attala and A.~Cavalcanti and J.~Woodcock},
title = {Modelling and Verifying Robotic Software that Uses
Neural Networks},
editor = {{\'A}brah{\'a}m, Erika and Dubslaff, Clemens and Tarifa, Silvia Lizeth Tapia},
booktitle = {Theoretical Aspects of Computing -- ICTAC 2023},
year = {2023},
publisher = {Springer},
pages = {15--35},
isbn = {978-3-031-47963-2},
url = {https://doi.org/10.1007/978-3-031-47963-2_3},
doi = {10.1007/978-3-031-47963-2_3}
}
We dedicate this paper with great respect and friendship to He Jifeng on the occasion of his 80th birthday. Our research group owes much to him. The authors have over 150 publications on unifying theories of programming (UTP), a research topic Jifeng created with Tony Hoare. Our objective is to recount the history of Circus (a combination of Z, CSP, Dijkstra’s guarded command language, and Morgan’s refinement calculus) and the development of Isabelle/UTP. Our paper is in two parts. (1) We first discuss the activities needed to model systems: we need to formalise data models and their behaviours. We survey our work on these two aspects in the context of Circus. (2) Secondly, we describe our practical implementation of UTP in Isabelle/HOL. Mechanising UTP theories is the basis of novel verification tools. We also discuss ongoing and future work related to (1) and (2). Many colleagues have contributed to these works, and we acknowledge their support.
@inbook{WoodcockCFOSZ23,
author = {J.~Woodcock and A.~Cavalcanti and S.~Foster and M.~Oliveira and A.~Sampaio and F.~Zeyda},
editor = {Bowen, Jonathan P. and Li, Qin and Xu, Qiwen},
title = {{UTP}, {Circus}, and {Isabelle}},
booktitle = {Theories of Programming and Formal Methods: Essays
Dedicated to Jifeng He on the Occasion of His 80th
Birthday},
year = {2023},
publisher = {Springer Nature Switzerland},
address = {Cham},
pages = {19--51},
isbn = {978-3-031-40436-8},
doi = {10.1007/978-3-031-40436-8_2},
url = {https://doi.org/10.1007/978-3-031-40436-8_2}
}
@inproceedings{AdamYACWM23,
author = {M.~Adam and K.~Ye and D.~A.~Anisi and A.~Cavalcanti and J.~Woodcock and R.~Morris},
booktitle = {2023 IEEE 19th International Conference on
Automation Science and Engineering (CASE)},
title = {Probabilistic Modelling and Safety Assurance of an
Agriculture Robot Providing Light-Treatment},
year = {2023},
pages = {1-7},
doi = {10.1109/CASE56687.2023.10260395}
}
In recent work, Cavalcanti and her group, including Miyazawa and Timmis, have developed a CSP-based framework for model-based engineering of robotic systems, called RoboStar. In this paper, we describe our current effort to ally RoboStar and RT-Tester, an award-winning tool that embodies many of Jan Peleska’s beautiful results on formal testing. With our work, RoboStar users can benefit from the testing infrastructure of RT-Tester to run simulations and tests generated using the RoboStar automated techniques. The testing primitives of RT-Tester simplify the implementation of test cases, and the RT-Tester execution engine provides state-of-the-art high-performance real-time facilities to carry out and report the traceable results of test experiments.
@inbook{CavalcantiMST2023,
author = {A.~Cavalcanti and A.~Miyazawa and U.~Schulze and J.~Timmis},
editor = {Haxthausen, Anne E. and Huang, Wen-ling and Roggenbach, Markus},
title = {Bringing {RoboStar} and {RT-Tester} Together},
booktitle = {Applicable Formal Methods for Safe Industrial
Products: Essays Dedicated to Jan Peleska on the
Occasion of His 65th Birthday},
year = {2023},
publisher = {Springer Nature Switzerland},
address = {Cham},
pages = {16--33},
isbn = {978-3-031-40132-9},
doi = {10.1007/978-3-031-40132-9_2},
url = {https://doi.org/10.1007/978-3-031-40132-9_2}
}
@inproceedings{HendryCCM23,
author = {H.~Hendry and M.~Chattington and A.~Cavalcanti and C.~McCall},
title = {Verification of a search-and-rescue drone with
humans in the loop},
booktitle = {Human Factors in Robots, Drones and Unmanned
Systems. AHFE (2023) International Conference},
year = {2023},
editor = {Ahram, Tareq and Karwowski, Waldemar},
volume = {93},
series = {AHFE Open Access},
publisher = {AHFE International, USA},
doi = {10.54941/ahfe1003753}
}
@inproceedings{CavalcantiH23,
author = {A.~Cavalcanti and R.~M.~Hierons},
title = {Challenges in testing of cyclic systems},
booktitle = {2023 27th International Conference on Engineering of
Complex Computer Systems (ICECCS)},
year = {2023},
pages = {1-6},
doi = {10.1109/ICECCS59891.2023.00010}
}
@article{MousaviCFDHKLRRTW23,
author = {M.~R.~Mousavi and A.~Cavalcanti and M.~Fisher and L.~A.~Dennis and R.~M.~Hierons and B.~Y.~Kaddouh and E.~L.{-}C.~Law and R.~C.~Richardson and J.~O.~Ringer and I.~Tyukin and J.~Woodcock},
title = {Trustworthy Autonomous Systems Through
Verifiability},
journal = {Computer},
volume = {56},
number = {2},
pages = {40--47},
year = {2023},
url = {https://doi.org/10.1109/MC.2022.3192206},
doi = {10.1109/MC.2022.3192206}
}
@article{BaxterCGH23,
author = {J.~Baxter and A.~Cavalcanti and M.~Gazda and R.~M.~Hierons},
title = {Testing using {CSP} Models: Time, Inputs, and
Outputs},
journal = {{ACM} Trans. Comput. Log.},
volume = {24},
number = {2},
pages = {17:1--17:40},
year = {2023},
doi = {10.1145/3572837}
}
@inproceedings{YamanBJCC23,
author = {S.~G.~Yaman and C.~Burholt and M.~Jones and R.~Calinescu and A.~Cavalcanti},
editor = {Lambers, Leen and Uchitel, Sebasti{\'{a}}n},
title = {Specification and Validation of Normative Rules for
Autonomous Agents},
booktitle = {Fundamental Approaches to Software Engineering -
26th International Conference, {FASE} 2023, Held as
Part of the European Joint Conferences on Theory and
Practice of Software, {ETAPS} 2023, Paris, France,
April 22-27, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13991},
pages = {241--248},
publisher = {Springer},
year = {2023},
doi = {10.1007/978-3-031-30826-0\_13}
}
@article{YeCFMW22,
month = oct,
author = {K.~Ye and A.~Cavalcanti and S.~Foster and A.~Miyazawa and J.~Woodcock},
title = {Probabilistic modelling and verification using
{RoboChart} and {PRISM}},
journal = {Software and Systems Modeling},
volume = {21},
number = {2},
pages = {667--716},
year = {2022},
doi = {10.1007/s10270-021-00916-8}
}
@article{TownsendPANCCHT22,
author = {B.~Townsend and C.~Paterson and T.~T.~Arvind and G.~Nemirovsky and R.~Calinescu and A.~Cavalcanti and I.~Habli and A.~Thomas},
title = {From Pluralistic Normative Principles to
Autonomous-Agent Rules},
journal = {Minds Mach.},
volume = {32},
number = {4},
pages = {683--715},
year = {2022},
doi = {10.1007/s11023-022-09614-w}
}
@article{BarnettCM22,
author = {W.~Barnett and A.~Cavalcanti and A.~Miyazawa},
title = {Architectural modelling for robotics: RoboArch and
the CorteX example},
journal = {Frontiers Robotics {AI}},
volume = {9},
year = {2022},
doi = {10.3389/frobt.2022.991637}
}
@article{KulikDLMSTW22,
author = {T.~Kulik and B.~Dongol and P.~G.~Larsen and H.~D.~Macedo and S.~Schneider and P.~W.~V.~Tran{-}J{\o}rgensen and J.~Woodcock},
title = {A Survey of Practical Formal Methods for Security},
journal = {Formal Aspects of Computing},
volume = {34},
number = {1},
pages = {1--39},
year = {2022},
url = {https://doi.org/10.1145/3522582},
doi = {10.1145/3522582}
}
RoboStar is a toolkit for model-based development using a domain-specific notation, RoboChart, with enriched UML-like state machines and a custom component model. We present RoboCert: a novel notation, based on UML sequence diagrams, which facilitates the specification of properties over RoboChart components. With RoboCert, we can express properties of a robotic system in a user-friendly, idiomatic manner. RoboCert specifications can be existential or universal, include timing notions such as deadlines and budgets, and both safety and liveness properties. Our work is faithful to UML where it can be, but presents significant extensions to fit the robotics application needs. RoboCert comes with tooling support for modelling and verification by model checking, and formal semantics in tock-CSP, the discrete-time variant of CSP.
@inproceedings{Windsor2022,
author = {M.~Windsor and A.~Cavalcanti},
editor = {A.~Riesco and M.~Zhang},
title = {{RoboCert}: Property Specification in Robotics},
booktitle = {Formal Methods and Software Engineering},
year = {2022},
publisher = {Springer},
pages = {386--403},
isbn = {978-3-031-17244-1},
url = {https://eprints.whiterose.ac.uk/192009/1/ICFEM_2022_windsor_cavalcanti_postprint.pdf},
doi = {10.1007/978-3-031-17244-1_23}
}
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.
@inproceedings{Ye2022,
author = {K.~Ye and S.~Foster and J.~Woodcock},
editor = {A.~Riesco and M.~Zhang},
title = {Formally Verified Animation for {RoboChart} Using
Interaction Trees},
booktitle = {Formal Methods and Software Engineering},
year = {2022},
publisher = {Springer},
pages = {404--420},
doi = {10.1007/978-3-031-17244-1_24},
isbn = {978-3-031-17244-1},
url = {https://eprints.whiterose.ac.uk/188566/1/Animation_of_RoboChart_with_interaction_trees_20220407_ICFEM2022.pdf}
}
@inproceedings{Yan0HW22,
author = {F.~Yan and S.~Foster and I.~Habli and R.~Wei},
editor = {L.~F.~Pires and S.~Hammoudi and E.~Seidewitz},
title = {Model-based Generation of Hazard-driven Arguments
and Formal Verification Evidence for Assurance
Cases},
booktitle = {Proceedings of the 10th International Conference on
Model-Driven Engineering and Software Development,
{MODELSWARD} 2022, Online Streaming, February 6-8,
2022},
pages = {252--263},
publisher = {{SCITEPRESS}},
year = {2022},
url = {https://eprints.whiterose.ac.uk/182058/1/MODELSWARD_2022_Model_based_AC_Generation_Camera_Ready_.pdf},
doi = {10.5220/0010847300003119}
}
As a general trend in industrial robotics, an increasing number of safety functions are being developed or re-engineered to be handled in software rather than by physical hardware such as safety relays or interlock circuits. This trend reinforces the importance of supplementing traditional, input-based testing and quality procedures which are widely used in industry today, with formal verification and model-checking methods. To this end, this paper focuses on a representative safety-critical system in an ABB industrial paint robot, namely the High-Voltage electrostatic Control system (HVC). The practical convergence of the high-voltage produced by the HVC, essential for safe operation, is formally verified using a novel and general co-verification framework where hardware and software models are related via platform mappings. This approach enables the pragmatic combination of highly diverse and specialised tools. The paper’s main contribution includes details on how hardware abstraction and verification results can be transferred between tools in order to verify system-level safety properties. It is noteworthy that the HVC application considered in this paper has a rather generic form of a feedback controller. Hence, the co-verification framework and experiences reported here are also highly relevant for any cyber-physical system tracking a setpoint reference.
@article{Murray2022,
title = {Safety assurance of an industrial robotic control
system using hardware/software co-verification},
journal = {Science of Computer Programming},
year = {2022},
issn = {0167-6423},
doi = {10.1016/j.scico.2021.102766},
url = {https://www.sciencedirect.com/science/article/pii/S0167642321001593},
author = {Y.~Murray and M.~Sirevåg and P.~Ribeiro and D.~A.~Anisi and M.~Mossige},
keywords = {Formal verification, Co-verification, Model
checking, High-Voltage Controller (HVC), Robots,
Cyber-Physical Systems (CPS)}
}
@inproceedings{FitzgeraldLMWG22,
author = {J.~S.~Fitzgerald and P.~G.~Larsen and T.~Margaria and J.~Woodcock and C.~Gomes},
editor = {T.~Margaria and B.~Steffen},
title = {Engineering of Digital Twins for Cyber-Physical
Systems},
booktitle = {Leveraging Applications of Formal Methods,
Verification and Validation. Practice - 11th
International Symposium, ISoLA 2022, Rhodes, Greece,
October 22-30, 2022, Proceedings, Part {IV}},
series = {Lecture Notes in Computer Science},
volume = {13704},
pages = {3--8},
publisher = {Springer},
year = {2022},
doi = {10.1007/978-3-031-19762-8\_1}
}
@inproceedings{WrightGW22,
author = {T.~Wright and C.~Gomes and J.~Woodcock},
editor = {T.~Margaria and B.~Steffen},
title = {Formally Verified Self-adaptation of an Incubator
Digital Twin},
booktitle = {Leveraging Applications of Formal Methods,
Verification and Validation. Practice - 11th
International Symposium, ISoLA 2022, Rhodes, Greece,
October 22-30, 2022, Proceedings, Part {IV}},
series = {Lecture Notes in Computer Science},
volume = {13704},
pages = {89--109},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-19762-8\_7},
doi = {10.1007/978-3-031-19762-8\_7}
}
@article{TownsendPANCCHT23,
author = {B.~Townsend and C.~Paterson and T.~T.~Arvind and G.~Nemirovsky and R.~Calinescu and A.~Cavalcanti and I.~Habli and A.~Thomas},
title = {From Pluralistic Normative Principles to
Autonomous-Agent Rules},
journal = {Minds Mach.},
volume = {32},
number = {4},
pages = {683--715},
year = {2022},
url = {https://doi.org/10.1007/s11023-022-09614-w},
doi = {10.1007/s11023-022-09614-w}
}
@inproceedings{Du0N22,
author = {D.~Du and A.~Cavalcanti and J.~Nie},
title = {{RoboSimVer}: {A} Tool for RoboSim Modeling and
Analysis},
booktitle = {37th {IEEE/ACM} International Conference on
Automated Software Engineering, {ASE} 2022,
Rochester, MI, USA, October 10-14, 2022},
pages = {164:1--164:4},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3551349.3559533},
doi = {10.1145/3551349.3559533}
}
@article{BaxterT21,
month = apr,
title = {Sound reasoning in tock-{CSP}},
author = {J.~Baxter and P.~Ribeiro and A.~Cavalcanti},
year = {2021},
journal = {Acta Informatica},
url = {https://eprints.whiterose.ac.uk/174356/},
doi = {10.1007/s00236-020-00394-3}
}
@inproceedings{LindosoNDL21,
author = {W.~Lindoso and S.~C.~Nogueira and R.~Domingues and L.~Lima},
editor = {S.~Campos and M.~Minea},
title = {Visual Specification of Properties for Robotic
Designs},
booktitle = {Formal Methods: Foundations and Applications - 24th
Brazilian Symposium, {SBMF} 2021, Virtual Event,
December 6-10, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13130},
pages = {34--52},
publisher = {Springer},
year = {2021},
doi = {10.1007/978-3-030-92137-8\_3}
}
@article{FosterNGWK21,
author = {S.~Foster and Y.~Nemouchi and M.~Gleirscher and R.~Wei and T.~Kelly},
title = {Integration of Formal Proof into Unified Assurance
Cases with Isabelle/SACM},
journal = {Formal Aspects Comput.},
volume = {33},
number = {6},
pages = {855--884},
year = {2021},
doi = {10.1007/s00165-021-00537-4},
url = {https://link.springer.com/article/10.1007/s00165-021-00537-4}
}
@inproceedings{AW2021,
author = {A.~Walter and S.~J.~Bale and A.~Tyrrell},
title = {Implementation of Reduced Precision Integer
Epigenetic Networks in Hardware},
booktitle = {IEEE SSCI 2021 (Symposium Series on Computational
Intelligence)},
publisher = {IEEE},
year = {2021},
url = {https://eprints.whiterose.ac.uk/182150/}
}
@inproceedings{CavalcantiBC21,
author = {A.~Cavalcanti and J.~Baxter and G.~Carvalho},
editor = {R.~Calinescu and C.~S.~Pasareanu},
title = {{RoboWorld}: Where Can My Robot Work?},
booktitle = {Software Engineering and Formal Methods - 19th
International Conference, {SEFM} 2021, Virtual
Event, December 6-10, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13085},
pages = {3--22},
publisher = {Springer},
year = {2021},
doi = {10.1007/978-3-030-92124-8\_1}
}
@inproceedings{AbbaCJ21,
author = {A.~Abba and A.~Cavalcanti and J.~Jacob},
editor = {S.~Campos and M.~Minea},
title = {Temporal Reasoning Through Automatic Translation of
tock-CSP into Timed Automata},
booktitle = {Formal Methods: Foundations and Applications - 24th
Brazilian Symposium, {SBMF} 2021, Virtual Event,
December 6-10, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13130},
pages = {70--86},
publisher = {Springer},
year = {2021},
doi = {10.1007/978-3-030-92137-8\_5}
}
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.
@inproceedings{Kangfeng2021,
author = {K.~Ye and S.~Foster and J.~Woodcock},
editor = {U.~Fahrenberg and M.~Gehrke and L.~Santocanale and M.~Winter},
title = {Automated Reasoning for Probabilistic Sequential
Programs with Theorem Proving},
booktitle = {Relational and Algebraic Methods in Computer
Science},
year = {2021},
publisher = {Springer International Publishing},
pages = {465--482},
isbn = {978-3-030-88701-8},
doi = {10.1007/978-3-030-88701-8_28},
url = {https://link.springer.com/content/pdf/10.1007%2F978-3-030-88701-8_28.pdf}
}
@article{GleirscherCW21,
author = {M.~Gleirscher and R.~Calinescu and J.~Woodcock},
title = {RiskStructures: {A} design algebra for risk-aware
machines},
journal = {Formal Aspects Computing},
volume = {33},
number = {4-5},
pages = {763--802},
year = {2021},
doi = {10.1007/s00165-021-00545-4}
}
@inproceedings{EsterlePW21,
author = {L.~Esterle and B.~Porter and J.~Woodcock},
editor = {E.~El{-}Araby and V.~Kalogeraki and D.~Pianini and F.~Lassabe and B.~Porter and S.~Ghahremani and I.~Nunes and M.~Bakhouya and S.~Tomforde},
title = {Verification and Uncertainties in Self-integrating
System},
booktitle = {{IEEE} International Conference on Autonomic
Computing and Self-Organizing Systems, {ACSOS} 2021,
Companion Volume, Washington, DC, USA, September 27
- Oct. 1, 2021},
pages = {220--225},
publisher = {{IEEE}},
year = {2021},
doi = {10.1109/ACSOS-C52956.2021.00050}
}
@inbook{Woodcock2021,
author = {J.~Woodcock},
title = {{H}oare and {H}e’s {Unifying Theories of
Programming}},
year = {2021},
isbn = {9781450387286},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
edition = {1},
doi = {10.1145/3477355.3477369},
booktitle = {{T}heories of {P}rogramming: {The Life and Works of
Tony Hoare}},
pages = {285–316},
numpages = {32}
}
@inproceedings{ZD13,
author = {M.~Zhang and D.~Du and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti and Filho, M.~Conserva and M.~Zhang},
title = {{Transforming RoboSim Models into UPPAAL}},
pages = {71--78},
booktitle = {15th International Symposium on Theoretical Aspects
of Software Engineering},
publisher = {IEEE},
year = {2021},
doi = {10.1109/TASE52547.2021.00037}
}
@inproceedings{Cav21,
author = {A.~L.~C.~Cavalcanti},
title = {{RoboStar Modelling Stack: Tackling the Reality
Gap}},
year = {2021},
publisher = {Association for Computing Machinery},
doi = {10.1145/3459086.3459628},
booktitle = {1st International Workshop on Verification of
Autonomous \& Robotic Systems},
series = {VARS 2021}
}
@book{CDHTW21,
editor = {A.~L.~C.~Cavalcanti and B.~Dongol and R.~Hierons and J.~Timmis and J.~C.~P.~Woodcock},
title = {Software Engineering for Robotics},
year = {2021},
publisher = {Springer International Publishing},
isbn = {978-3-030-66493-0},
doi = {10.1007/978-3-030-66494-7},
url = {https://www.springer.com/gp/book/9783030664930}
}
@inbook{CBBCFMRS21,
author = {A.~L.~C.~Cavalcanti and W.~Barnett and J.~Baxter and G.~Carvalho and M.~C.~Filho and A.~Miyazawa and P.~Ribeiro and A.~C.~A.~Sampaio},
editor = {A.~L.~C.~Cavalcanti and B.~Dongol and R.~Hierons and J.~Timmis and J.~C.~P.~Woodcock},
title = {RoboStar Technology: A Roboticist's Toolbox for
Combined Proof, Simulation, and Testing},
booktitle = {Software Engineering for Robotics},
year = {2021},
publisher = {Springer International Publishing},
pages = {249--293},
doi = {10.1007/978-3-030-66494-7_9},
url = {https://www-users.york.ac.uk/%7Ealcc500/publications/papers/CBBCFMRS21.pdf}
}
@article{ChenLWW21,
author = {X.~Chen and Z.~Liu and J.~Wang and J.~Woodcock},
title = {Editorial},
journal = {Formal Aspects Comput.},
volume = {33},
number = {3},
pages = {299--300},
year = {2021},
url = {https://doi.org/10.1007/s00165-021-00552-5},
doi = {10.1007/s00165-021-00552-5}
}
@article{ZhaoZCLW21,
author = {H.~Zhao and X.~Zeng and T.~Chen and Z.~Liu and J.~Woodcock},
title = {Learning safe neural network controllers with
barrier certificates},
journal = {Formal Aspects Comput.},
volume = {33},
number = {3},
pages = {437--455},
year = {2021},
url = {https://doi.org/10.1007/s00165-021-00544-5},
doi = {10.1007/s00165-021-00544-5}
}
@article{VinkC21,
author = {E.~P.~de~Vink and A.~Cavalcanti},
title = {Editorial},
journal = {Formal Aspects Comput.},
volume = {33},
number = {1},
pages = {1--2},
year = {2021},
url = {https://doi.org/10.1007/s00165-020-00522-3},
doi = {10.1007/s00165-020-00522-3}
}
@article{FosterYCW21,
author = {S.~Foster and K.~Ye and A.~Cavalcanti and J.~Woodcock},
title = {Automated verification of reactive and concurrent
programs by calculation},
journal = {J. Log. Algebraic Methods Program.},
volume = {121},
pages = {100681},
year = {2021},
url = {https://doi.org/10.1016/j.jlamp.2021.100681},
doi = {10.1016/j.jlamp.2021.100681}
}
@inproceedings{ACW20,
author = {Z.~Attala and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
editor = {A.~Albarghouthi and G.~Katz and N.~Narodytska},
title = {{A Comparison of Neural Network Tools for the
Verification of Linear Specifications of ReLU
Networks}},
booktitle = {3rd Workshop on Formal Methods for ML-Enabled
Autonomous System},
pages = {22--33},
year = {2020},
url = {https://fomlas2020.wixsite.com/fomlas2020}
}
@article{LecomteDFO20,
author = {T.~Lecomte and D.~D{\'{e}}harbe and P.~Fournier and M.~Oliveira},
title = {The {CLEARSY} safety platform: 5 years of research,
development and deployment},
journal = {Sci. Comput. Program.},
volume = {199},
pages = {102524},
year = {2020},
doi = {10.1016/j.scico.2020.102524}
}
@article{ChangWZWWB20,
author = {W.~Chang and R.~Wei and S.~Zhao and A.~J.~Wellings and J.~Woodcock and A.~Burns},
title = {Development Automation of Real-Time Java:
Model-Driven Transformation and Synthesis},
journal = {{ACM} Trans. Embed. Comput. Syst.},
volume = {19},
number = {5},
pages = {31:1--31:26},
year = {2020},
url = {https://eprints.whiterose.ac.uk/159681/1/TECS_From_Java_to_Real_Time_Java_A_Model_Driven_Methodology.pdf},
doi = {10.1145/3391897},
timestamp = {Fri, 04 Dec 2020 16:04:20 +0100}
}
@article{CavalcantiHN20,
author = {A.~Cavalcanti and Hierons, R.~M. and Nogueira, S.~C.},
title = {Inputs and Outputs in {CSP:} {A} Model and a Testing
Theory},
journal = {{ACM} Trans. Comput. Log.},
volume = {21},
number = {3},
pages = {24:1--24:53},
year = {2020},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/CHN20.pdf},
doi = {10.1145/3379508},
timestamp = {Tue, 17 Nov 2020 16:08:03 +0100}
}
@inproceedings{CavalcantiABZ20,
author = {A.~Cavalcanti},
title = {Modelling and Verification of Robotic Platforms for
Simulation Using RoboStar Technology},
booktitle = {Rigorous State-Based Methods - 7th International
Conference, {ABZ} 2020, Ulm, Germany, May 27-29,
2020, Proceedings},
pages = {3--5},
year = {2020},
crossref = {DBLP:conf/asm/2020},
doi = {10.1007/978-3-030-48077-6\_1},
timestamp = {Mon, 25 May 2020 12:33:39 +0200}
}
@article{FosterBCWZ20,
author = {S.~Foster and J.~Baxter and A.~Cavalcanti and J.~Woodcock and F.~Zeyda},
title = {Unifying semantic foundations for automated
verification tools in Isabelle/UTP},
journal = {Sci. Comput. Program.},
volume = {197},
pages = {102510},
year = {2020},
url = {https://arxiv.org/abs/1905.05500},
doi = {10.1016/j.scico.2020.102510},
timestamp = {Tue, 29 Dec 2020 18:17:44 +0100}
}
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.
@inbook{Ye2020,
author = {K.~Ye and S.~Foster and J.~Woodcock},
editor = {Adamatzky, Andrew and Kendon, Vivien},
title = {Compositional Assume-Guarantee Reasoning of Control
Law Diagrams Using UTP},
booktitle = {From Astrophysics to Unconventional Computation:
Essays Presented to Susan Stepney on the Occasion of
her 60th Birthday},
year = {2020},
publisher = {Springer International Publishing},
pages = {215--254},
isbn = {978-3-030-15792-0},
doi = {10.1007/978-3-030-15792-0_10}
}
@inproceedings{FosterFSE2020,
author = {S.~Foster and Y.~Nemouchi and C.~O'Halloran and K.~Stephenson and N.~Tudor},
title = {Formal Model-Based Assurance Cases in Isabelle/SACM:
An Autonomous Underwater Vehicle Case Study},
booktitle = {FormaliSE@ICSE 2020: 8th International Conference on
Formal Methods in Software Engineering, Seoul,
Republic of Korea, July 13, 2020},
pages = {11--21},
year = {2020},
url = {https://pure.york.ac.uk/portal/services/downloadRegister/64250950/FormaliSE2020.pdf},
doi = {10.1145/3372020.3391559},
timestamp = {Tue, 22 Sep 2020 14:35:32 +0200}
}
@inproceedings{Murray2020,
author = {Y.~Murray and D.~A.~Anisi and M.~Sirev{\aa}g and P.~Ribeiro and R.S.~Hagag},
title = {Safety Assurance of a High Voltage Controller for an
Industrial Robotic System},
booktitle = {Formal Methods: Foundations and Applications - 23rd
Brazilian Symposium, {SBMF} 2020, Ouro Preto,
Brazil, November 25-27, 2020, Proceedings},
pages = {45--63},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-63882-5\_4},
doi = {10.1007/978-3-030-63882-5\_4},
timestamp = {Tue, 01 Dec 2020 09:11:54 +0100}
}
@inproceedings{FosterMS20,
author = {S.~Foster and J.~J.~Huerta~y~Munive and G.~Struth},
title = {Differential Hoare Logics and Refinement Calculi for
Hybrid Systems with Isabelle/HOL},
booktitle = {Relational and Algebraic Methods in Computer Science
- 18th International Conference, RAMiCS 2020,
Palaiseau, France, April 8-11, 2020, Proceedings },
pages = {169--186},
year = {2020},
url = {https://eprints.whiterose.ac.uk/155734/1/hybrid_kat.pdf},
doi = {10.1007/978-3-030-43520-2\_11},
timestamp = {Wed, 01 Apr 2020 16:27:12 +0200}
}
@inproceedings{FosterB20,
author = {S.~Foster and J.~Baxter},
title = {Automated Algebraic Reasoning for Collections and
Local Variables with Lenses},
booktitle = {Relational and Algebraic Methods in Computer Science
- 18th International Conference, RAMiCS 2020,
Palaiseau, France, April 8-11, 2020, Proceedings },
pages = {100--116},
year = {2020},
url = {https://eprints.whiterose.ac.uk/155413/15/RAMiCS2020.pdf},
doi = {10.1007/978-3-030-43520-2\_7},
timestamp = {Thu, 09 Apr 2020 21:56:54 +0200}
}
@article{GleirscherFW20,
author = {M.~Gleirscher and S.~Foster and J.~C.~P.~Woodcock},
title = {New Opportunities for Integrated Formal Methods},
journal = {{ACM} Comput. Surv.},
volume = {52},
number = {6},
pages = {117:1--117:36},
year = {2020},
url = {https://eprints.whiterose.ac.uk/149059/8/1812_10103.pdf},
doi = {10.1145/3357231},
timestamp = {Fri, 24 Jan 2020 16:59:44 +0100}
}
@article{FosterCCWZ20,
author = {S.~Foster and A.~L.~C.~Cavalcanti and S.~Canham and J.~C.~P.~Woodcock and Zeyda, Frank},
title = {Unifying theories of reactive design contracts},
journal = {Theor. Comput. Sci.},
volume = {802},
pages = {105--140},
year = {2020},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/FCCWZ20.pdf},
doi = {10.1016/j.tcs.2019.09.017},
timestamp = {Mon, 02 Dec 2019 18:19:21 +0100}
}
@inproceedings{Ribeiro2020,
author = {P.~Ribeiro},
title = {A Unary Semigroup Trace Algebra},
booktitle = {Relational and Algebraic Methods in Computer Science
- 18th International Conference, RAMiCS 2020,
Palaiseau, France, April 8-11, 2020, Proceedings },
year = {2020},
volume = {12062},
pages = {270--285},
url = {https://eprints.whiterose.ac.uk/156604/1/RAMiCS2020.pdf},
doi = {10.1007/978-3-030-43520-2\_17},
timestamp = {Thu, 09 Apr 2020 21:56:54 +0200}
}
Robots are becoming ubiquitous: from vacuum cleaners to driverless cars, there is a wide variety of applications, many with potential safety hazards. The work presented in this paper proposes a set of constructs suitable for both modelling robotic applications and supporting verification via model checking and theorem proving. Our goal is to support roboticists in writing models and applying modern verification techniques using a language familiar to them. To that end, we present RoboChart, a domain-specific modelling language based on UML, but with a restricted set of constructs to enable a simplified semantics and automated reasoning. We present the RoboChart metamodel, its well-formedness rules, and its process-algebraic semantics. We discuss verification based on these foundations using an implementation of RoboChart and its semantics as a set of Eclipse plug-ins called RoboTool.
@article{Miyazawa2019,
author = {A.~Miyazawa and P.~Ribeiro and L.~Wei and A.~L.~C.~Cavalcanti and J.~Timmis and J.~C.~P.~Woodcock},
title = {RoboChart: modelling and verification of the
functional behaviour of robotic applications},
journal = {Software {\&} Systems Modeling},
year = {2019},
month = jan,
day = {23},
issn = {1619-1374},
volume = {18},
pages = {3097--3149},
doi = {10.1007/s10270-018-00710-z},
url = {https://doi.org/10.1007/s10270-018-00710-z}
}
@inproceedings{Nemouchi0GK19,
author = {Y.~Nemouchi and S.~Foster and M.~Gleirscher and T.~Kelly},
title = {Isabelle/SACM: Computer-Assisted Assurance Cases
with Integrated Formal Methods},
booktitle = {Integrated Formal Methods - 15th International
Conference, {IFM} 2019, Bergen, Norway, December
2-6, 2019, Proceedings},
pages = {379--398},
year = {2019},
crossref = {DBLP:conf/ifm/2019},
url = {https://doi.org/10.1007/978-3-030-34968-4\_21},
doi = {10.1007/978-3-030-34968-4\_21},
timestamp = {Fri, 22 Nov 2019 14:00:20 +0100}
}
@inproceedings{GleirscherFN19,
author = {M.~Gleirscher and S.~Foster and Y.~Nemouchi},
title = {Evolution of Formal Model-Based Assurance Cases for
Autonomous Robots},
booktitle = {Software Engineering and Formal Methods - 17th
International Conference, {SEFM} 2019, Oslo, Norway,
September 18-20, 2019, Proceedings},
pages = {87--104},
year = {2019},
crossref = {DBLP:conf/sefm/2019},
url = {https://doi.org/10.1007/978-3-030-30446-1\_5},
doi = {10.1007/978-3-030-30446-1\_5},
timestamp = {Mon, 23 Sep 2019 17:27:12 +0200}
}
@inproceedings{WoodcockC00Y19,
author = {J.~Woodcock and A.~Cavalcanti and S.~Foster and A.~Mota and K.~Ye},
title = {Probabilistic Semantics for RoboChart - {A} Weakest
Completion Approach},
booktitle = {Unifying Theories of Programming - 7th International
Symposium, {UTP} 2019, Dedicated to Tony Hoare on
the Occasion of His 85th Birthday, Porto, Portugal,
October 8, 2019, Proceedings},
pages = {80--105},
year = {2019},
crossref = {DBLP:conf/utp/2019},
url = {https://doi.org/10.1007/978-3-030-31038-7\_5},
doi = {10.1007/978-3-030-31038-7\_5},
timestamp = {Sat, 12 Oct 2019 12:51:37 +0200}
}
@inproceedings{Foster19,
author = {S.~Foster},
title = {Hybrid Relations in Isabelle/UTP},
booktitle = {Unifying Theories of Programming - 7th International
Symposium, {UTP} 2019, Dedicated to Tony Hoare on
the Occasion of His 85th Birthday, Porto, Portugal,
October 8, 2019, Proceedings},
pages = {130--153},
year = {2019},
crossref = {DBLP:conf/utp/2019},
url = {https://doi.org/10.1007/978-3-030-31038-7\_7},
doi = {10.1007/978-3-030-31038-7\_7},
timestamp = {Sat, 12 Oct 2019 12:51:37 +0200}
}
@article{PeleskaHC19,
author = {J.~Peleska and W.~Huang and A.~Cavalcanti},
title = {Finite complete suites for {CSP} refinement testing},
journal = {Sci. Comput. Program.},
volume = {179},
pages = {1--23},
year = {2019},
url = {https://doi.org/10.1016/j.scico.2019.04.004},
doi = {10.1016/j.scico.2019.04.004},
timestamp = {Fri, 05 Jul 2019 09:38:13 +0200}
}
@inproceedings{CavalcantiBHL19,
author = {A.~Cavalcanti and J.~Baxter and R.~M.~Hierons and R.~Lefticaru},
title = {Testing Robots Using {CSP}},
booktitle = {Tests and Proofs - 13th International Conference,
{TAP} 2019, Held as Part of the Third World Congress
on Formal Methods 2019, Porto, Portugal, October
9-11, 2019, Proceedings},
pages = {21--38},
year = {2019},
crossref = {DBLP:conf/tap/2019},
url = {https://doi.org/10.1007/978-3-030-31157-5\_2},
doi = {10.1007/978-3-030-31157-5\_2},
timestamp = {Mon, 23 Sep 2019 14:04:40 +0200}
}
@inproceedings{HoareSW19,
author = {T.~Hoare and G.~Struth and J.~Woodcock},
title = {A Calculus of Space, Time, and Causality: Its
Algebra, Geometry, Logic},
booktitle = {Unifying Theories of Programming - 7th International
Symposium, {UTP} 2019, Dedicated to Tony Hoare on
the Occasion of His 85th Birthday, Porto, Portugal,
October 8, 2019, Proceedings},
pages = {3--21},
year = {2019},
crossref = {DBLP:conf/utp/2019},
url = {https://doi.org/10.1007/978-3-030-31038-7\_1},
doi = {10.1007/978-3-030-31038-7\_1},
timestamp = {Mon, 23 Sep 2019 14:19:07 +0200}
}
Demonic and angelic nondeterminism play fundamental roles as abstraction mechanisms for formal modelling. In contrast with its demonic counterpart, in an angelic choice failure is avoided whenever possible. Although it has been extensively studied in refinement calculi, in the context of process algebras, and of the Communicating Sequential Processes (CSP) algebra for refinement, in particular, it has been elusive. We show here that a semantics for an extended version of CSP that includes both demonic and angelic choice can be provided using Hoare and He’s Unifying Theories of Programming (UTP). Since CSP is given semantics in the UTP via reactive designs (pre and postcondition pairs) we have developed a theory of angelic designs and a conservative extension of the CSP theory using reactive angelic designs. To characterise angelic nondeterminism appropriately in an algebra of processes, however, a notion of divergence that can undo the history of events needs to be considered. Taking this view, we present a model for CSP where angelic choice completely avoids divergence just like in the refinement calculi for sequential programs.
@article{Ribeiro2019a,
groups = {papers},
keywords = { Semantics, Formal specification, Process algebras,
CSP, UTP },
author = {P.~Ribeiro and A.~L.~C.~Cavalcanti},
url = {https://www-users.cs.york.ac.uk/%7Epfr/publications/TCS2018.pdf},
doi = {10.1016/j.tcs.2018.10.008},
issn = {0304-3975},
year = {2019},
pages = {19-63},
volume = {756},
journal = {Theoretical Computer Science},
title = {Angelic processes for CSP via the UTP}
}
Safety-Critical Java (SCJ) is a version of Java for real-time, embedded, safety-critical applications. It supports certification via abstractions that enforce a particular program architecture, with controlled concurrency and memory models. SCJ is an Open Group standard, with a reference implementation, but little support for reasoning. Here, we present SCJ-Circus, a refinement notation for specification and verification of low-level models of SCJ programs. SCJ-Circus is part of the Circus family of state-rich process algebras: it includes the Circus constructs for modelling of sequential and concurrent behaviour based on Z and CSP, and the real-time and object-oriented extensions of Circus, in addition to the SCJ abstractions. We present the syntax of SCJ-Circus and its semantics, defined by mapping SCJ-Circus constructs to those of Circus. We also detail a refinement strategy that takes a Circus design that adheres to a multiprocessor cyclic executive pattern and produces an SCJ program design, described in SCJ-Circus. Finally, we show how this refinement strategy can be extended for more complex program architectures.
@article{Miyazawa2019a,
groups = { hijac, papers },
keywords = { SCJ, missions, event handlers, process algebra,
semantics, refinement },
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti and A.~Wellings},
url = {http://www.sciencedirect.com/science/article/pii/S0167642319300012},
doi = {10.1016/j.scico.2019.01.002},
issn = {0167-6423},
year = {2019},
journal = {Science of Computer Programming},
title = {SCJ-Circus: specification and refinement of
Safety-Critical Java programs}
}
Simulation is a favoured technique for analysis of robotic systems. Currently, however, simulations are programmed in an ad hoc way, for specific simulators, using either proprietary languages or general languages like C or C++. Even when a higher-level language is used, no clear relation between the simulation and a design model is established. We describe a tool-independent notation called RoboSim, designed specifically for modelling of (verified) simulations. We describe the syntax, well-formedness conditions, and semantics of RoboSim. We also show how we can use RoboSim models to check if a simulation is consistent with a functional design written in a UML-like notation akin to those often used by practitioners on an informal basis. We show how to check whether the design enables a feasible scheduling of behaviours in cycles as needed for a simulation, and formalise implicit assumptions routinely made when programming simulations. We develop a running example and three additional case studies to illustrate RoboSim and the proposed verification techniques. Tool support is also briefly discussed. Our results enable the description of simulations using tool-independent diagrammatic models amenable to verification and automatic generation of code.
@article{Cavalcanti2019a,
groups = { robocalc, papers },
keywords = { State machines, Process algebra, CSP, Semantics,
Refinement },
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and A.~Miyazawa and P.~Ribeiro and M.~S.~Conserva~Filho and A.~Didier and W.~Li and J.~Timmis},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/CSMRCD19.pdf},
doi = {10.1016/j.scico.2019.01.004},
issn = {0167-6423},
year = {2019},
pages = {1-37},
volume = {174},
journal = {Science of Computer Programming},
title = {Verified simulation for robotics}
}
Hoare and He’s theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to consider continuous-time traces and thereby facilitate models of hybrid systems. We then use this algebra to reconstruct the theory of reactive processes in our generic setting, and prove characteristic laws for sequential and parallel processes, all of which have been mechanically verified in the Isabelle/HOL proof assistant.
@article{FCWZ18,
title = {Unifying theories of time with generalised reactive
processes },
journal = {Information Processing Letters},
volume = {135},
pages = {47 - 52},
month = jul,
year = {2018},
doi = {10.1016/j.ipl.2018.02.017},
author = {S.~Foster and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and F.~Zeyda}
}
The success of component-based techniques for software construction relies on trust in the emergent behaviour of the compositions. Here, we propose an efficient correct-by-construction technique for building livelock-free CSP models. Its verification conditions are based on a local analysis of the shortest event sequences (traces) that represent a recursive behaviour in the CSP model. This affords significant gains in performance in model checking. We evaluate our strategy based on models of the Milner’s scheduler and the dining philosophers.
@article{COSC18,
title = {Compositional and Local Livelock Analysis for {CSP}},
pages = {21 - 25},
journal = {Information Processing Letters},
volume = {133},
issn = {0020-0190},
month = may,
year = {2018},
doi = {10.1016/j.ipl.2017.12.011},
author = {M.~S.~Conserva~Filho and M.~V.~M.~Oliveira and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti}
}
@inproceedings{Foster2018a,
groups = { robocalc, isabelle-utp, papers },
publisher = {Springer International Publishing},
address = { Cham },
pages = {137--155},
year = {2018},
booktitle = {Formal Aspects of Component Software},
title = {Automating Verification of State Machines with
Reactive Designs and Isabelle/UTP},
url = {https://pure.york.ac.uk/portal/services/downloadRegister/55606873/1807.08588.pdf},
doi = {10.1007/978-3-030-02146-7_7},
author = {S.~Foster and J.~Baxter and A.~L.~C.~Cavalcanti and A.~Miyazawa and J.~C.~P.~Woodcock}
}
RoboChart is a graphical domain-specific language, based on UML, but tailored for the modelling and verification of single robot systems. In this paper, we introduce RoboChart facilities for modelling and verifying heterogeneous collections of interacting robots. We propose a new construct that describes the collection itself, and a new communication construct that allows fine-grained control over the communication patterns of the robots. Using these novel constructs, we apply RoboChart to model a simple yet powerful and widely used algorithm to maintain the aggregation of a swarm. Our constructs can be useful also in the context of other diagrammatic languages, including UML, to describe collections of arbitrary interacting entities.
@inproceedings{Cavalcanti2018a,
groups = { robocalc, papers },
isbn = { 978-3-319-98938-9 },
pages = {1--19},
address = {Cham},
publisher = {Springer International Publishing},
year = {2018},
booktitle = {Integrated Formal Methods},
title = {Modelling and Verification for Swarm Robotics},
author = {A.~L.~C.~Cavalcanti and A.~Miyazawa and A.~C.~A.~Sampaio and W.~Li and P.~Ribeiro and J.~Timmis}
}
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.
@inproceedings{Foster2018b,
groups = { papers },
isbn = { 978-3-030-02149-8 },
pages = {205--224},
address = {Cham},
publisher = {Springer International Publishing},
year = {2018},
booktitle = {Relational and Algebraic Methods in Computer
Science},
title = {Calculational Verification of Reactive Programs with
Reactive Relations and Kleene Algebra},
url = {https://pure.york.ac.uk/portal/services/downloadRegister/55512660/RAMICS2018.pdf},
doi = {10.1007/978-3-030-02149-8},
author = {S.~Foster and K.~Ye and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock}
}
Cosimulation techniques are popular in the design and early testing of cyber-physical systems. Such systems are typically composed of heterogeneous components and specified using a variety of languages and tools; this makes their formal analysis beyond simulation challenging. We here present work on formalised models and proofs about cosimulations in our theorem prover Isabelle/UTP, illustrated by an industrial case study from the railways sector. Novel contributions are a mechanised encoding of the FMI framework for cosimulation, simplification and translation of (case-study) models into languages supported by our proof system, and an encoding of an FMI instantiation.
@inproceedings{ZOFC18,
author = {F.~Zeyda and J.~Ouy and S.~Foster and A.~L.~C.~Cavalcanti},
title = {Formalising Cosimulation Models},
booktitle = {Software Engineering and Formal Methods - {SEFM}
2017 Collocated Workshops},
pages = {453--468},
doi = {10.1007/978-3-319-74781-1_31},
editor = {A.~Cerone and M.~Roveri},
series = {Lecture Notes in Computer Science},
volume = {10729},
publisher = {Springer},
year = {2018},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/ZOFC18.pdf}
}
High-level controllers for autonomous robotic systems can be specified using state machines. However, these are typically developed in an ad hoc manner without formal semantics, which makes it difficult to analyse the controller. Simulations are often used during the development, but a rigorous connection between the designed controller and the implementation is often overlooked. This paper presents a state-machine based notation, RoboChart, together with tools to automatically create code from the state machines, establishing a rigorous connection between specification and implementation. In RoboChart, the robot’s controller is specified either graphically or using a textual description language. The controller code for simulation is automatically generated through a direct mapping from the specification. We demonstrate our approach using two case studies (self-organized aggregation and swarm taxis) in swarm robotics. The simulations are presented using two different simulators showing the general applicability of our approach in a wide range of robotic controllers.
@inbook{Li-etal2016,
title = {From formalised state machines to implementation of
robotic controllers},
author = {W.~Li and A.~Miyazawa and P.~Ribeiro and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and J.~Timmis},
booktitle = {Distributed Autonomous Robotic Systems: The 13th
International Symposium},
year = {2018},
pages = {517--529},
doi = {10.1007/978-3-319-73008-0_36},
isbn = {978-3-319-73008-0},
series = {Springer Tracts in Advanced Robotics},
publisher = {Springer International Publishing},
editor = {Gro{\ss}, Roderich and Kolling, Andreas and Berman, Spring and Frazzoli, Emilio and Martinoli, Alcherio and Matsuno, Fumitoshi and Gauci, Melvin"},
url = {https://arxiv.org/abs/1702.01783}
}
Robotic systems have applications in many real-life scenarios, ranging from household cleaning to critical operations. RoboChart is a graphical language for describing robotic controllers designed specifically for autonomous and mobile robots, providing architectural constructs to identify the requirements for a robotic platform. It also provides a formal semantics in CSP. RoboChart has a probabilistic operator () but no associated probabilistic CSP semantics. When is used, currently a non-deterministic choice () is used as semantics; this is a conservative semantics but it does not allow the analysis of stochastic properties. In this paper we define the semantics of the operator in terms of the probabilistic CSP operator }}\backslashboxplus }}. We also show how this augmented CSP semantics for RoboChart can be translated into the PRISM probabilistic language to be able to check stochastic properties.
@inproceedings{ConservaFilho2018,
author = {Conserva Filho, M. S. and Marinho, R. and Mota, A. and Woodcock, J.},
title = {Analysing RoboChart with Probabilities},
booktitle = {Formal Methods: Foundations and Applications},
year = {2018},
editor = {Massoni, Tiago and Mousavi, Mohammad Reza},
pages = {198--214},
address = {Cham},
publisher = {Springer International Publishing},
isbn = {978-3-030-03044-5},
owner = {wv8579},
timestamp = {2019.09.26}
}
Software engineering for modern robot applications needs attention; current practice suffers from costly iterations of trial and error, with hardware and environment in the loop. We propose the adoption of an approach to simulation and co-simulation of robotics applications where designs and (co-)simulations are amenable to verification. In this approach, designs are composed of several (co-)models whose relationship is defined using a SysML profile. Simulation is the favoured technique for analysis in industry, and co-simulation enables the orchestrated use of a variety of simulation tools, including, for instance, reactive simulators and simulators of control laws. Here, we define the SysML profile that we propose and give it a process algebraic semantics. With that semantics, we capture the properties of the SysML model that must be satisfied by a co-simulation. Our long-term goal is to support validation and verification beyond what can be achieved with simulation.
@incollection{CMPW17,
author = {A.~L.~C.~Cavalcanti and A.~Miyazawa and R.~Payne and J.~Woodcock},
editor = {M.~Mazzara and B.~Meyer},
title = {Sound Simulation and Co-simulation for Robotics},
booktitle = {Present and Ulterior Software Engineering},
year = {2017},
publisher = {Springer International Publishing},
pages = {173--194},
doi = {10.1007/978-3-319-67425-4_11},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/CMPW17.pdf}
}
Nondeterminism is an inevitable constituent of any theory that describes concurrency. For the validation and verification of concurrent systems, it is essential to investigate the presence or absence of nondeterminism, just as much as deadlock or livelock. CSP is a well established process algebra; the main tool for practical use of CSP, the model checker FDR, checks determinism using a global analysis. We propose a local analysis, in order to improve performance and scalability. Our strategy is to use a compositional approach where we start from basic deterministic processes and check whether any of the composition operators introduce nondeterminism. We present the algorithms used in our strategy and experiments that show the efficiency of our approach.
@inproceedings{OCS17,
author = {R.~Otoni and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
editor = {S.~Cavalheiro and J.~Fiadeiro},
title = {Local Analysis of Determinism for CSP},
booktitle = {Formal Methods: Foundations and Applications},
year = {2017},
publisher = {Springer International Publishing},
pages = {107--124},
volume = {10623},
series = {Lecture Notes in Computer Science},
doi = {10.1007/978-3-319-70848-5_8},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/OCS17.pdf}
}
Robot software controllers are often concurrent and time critical, and requires modern engineering approaches for validation and verification. With this motivation, we have developed a tool and techniques for graphical modelling with support for automatic generation of underlying mathematical definitions for model checking. It is possible to check automatically both general properties, like absence of deadlock, and specific application properties. We cater both for timed and untimed modelling and verification. Our approach has been tried in examples used in a variety of robotic applications.
@inproceedings{MRLCT17,
author = {A.~Miyazawa and P.~Ribeiro and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis},
title = {Automatic Property Checking of Robotic Applications},
year = {2017},
booktitle = {The International Conference on Intelligent Robots
and Systems},
pages = {3869-3876},
doi = {10.1109/IROS.2017.8206238}
}
Designing robotic systems can be very challenging, yet controllers are often specified using informal notations with development driven primarily by simulations and physical experiments, without relation to abstract models of requirements. The ability to perform formal analysis and replicate results across different robotic platforms is hindered by the lack of well-defined formal notations. In this paper we present a timed state-machine based formal notation for robotics that is informed by current practice. We motivate our work with an example from swarm robotics and define a compositional CSP-based discrete timed semantics suitable for refinement. Our results support verification and, importantly, enable rigorous connection with sound simulations and deployments.
@inproceedings{Ribeiro2017,
author = {P.~Ribeiro and A.~Miyazawa and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis},
editor = {N.~Polikarpova and S.~Schneider},
title = {Modelling and Verification of Timed Robotic
Controllers},
booktitle = {Integrated Formal Methods},
year = {2017},
publisher = {Springer},
pages = {18--33},
doi = {10.1007/978-3-319-66845-1_2},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/RMLCT17.pdf},
isbn = {978-3-319-66845-1}
}
Simulation is a favoured technique for analysis of cyberphysical systems. With their increase in complexity, co-simulation, which involves the coordinated use of heterogeneous models and tools, has become widespread. An industry standard, FMI, has been developed to support orchestration; we provide the first behavioural semantics of FMI. We use the state-rich process algebra, Circus, to present our modelling approach, and indicate how models can be automatically generated from a description of the individual simulations and their dependencies. We illustrate the work using three algorithms for orchestration. A stateless version of the models can be verified using model checking via translation to CSP. With that, we can prove important properties of these algorithms, like termination and determinism, for example. We also show that the example provided in the FMI standard is not a valid algorithm.
@inproceedings{CWA16,
booktitle = {International Colloquium on Theoretical Aspects of
Computing},
title = {{Behavioural Models for FMI Co-simulations}},
editor = {A.~C.~A.~Sampaio and F.~Wang},
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and N.~Am\'alio},
year = {2016},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
doi = {10.1007/978-3-319-46750-4_15},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/CWA16.pdf}
}
We describe our work on a UTP semantics for the dynamic systems modelling language Modelica. This is a language for modelling a system’s continuous behaviour using a combination of differential-algebraic equations and an event-handling system. We develop a novel UTP theory of hybrid relations, inspired by Hybrid CSP and Duration Calculus, that is purely relational and provides uniform handling of continuous and discrete variables. This theory is mechanised in our Isabelle implementation of the UTP, Isabelle/UTP, with which we verify some algebraic properties. Finally, we show how a subset of Modelica models can be given semantics using our theory. When combined with the wealth of existing UTP theories for discrete system modelling, our work enables a sound approach to heterogeneous semantics for Cyber-Physical systems by leveraging the theory linking facilities of the UTP.
@inproceedings{FTCW16,
booktitle = {Unifying Theories of Programming},
title = {{Towards a UTP semantics for Modelica}},
author = {S.~Foster and B.~Thiele and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
year = {2016},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
doi = {10.1007/978-3-319-52228-9_3},
url = {http://eprints.whiterose.ac.uk/105107/1/utp2016.pdf}
}
Formal modelling of complex systems requires catering for a variety of aspects. The Unifying Theories of Programming (UTP) distinguishes itself as a semantic framework that promotes unification of results across different modelling paradigms via linking functions. The naive composition of theories, however, may yield unexpected or undesirable semantic models. Here, we propose a stepwise approach to linking theories where we deal separately with the definition of the relation between the variables in the different theories and the identification of healthiness conditions. We explore this approach by deriving healthiness conditions for Circus Time via calculation, based on the healthiness conditions of CSP and a small set of principles underlying the timed model.
@incollection{Ribeiro2016,
title = {{A} {S}tepwise {A}pproach to {L}inking {T}heories},
author = {P.~Ribeiro and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
booktitle = {{U}nifying {T}heories of {P}rogramming},
publisher = {Springer International Publishing},
year = {2016},
doi = {10.1007/978-3-319-52228-9_7},
series = {{L}ecture {N}otes in {C}omputer {S}cience},
url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/RCW17.pdf}
}
@thesis{HenrikNordlie,
author = {H.~Nordlie},
title = {Formal verification of synchronization properties of a multi-robot welding system},
publisher = {Norwegian University of Life Sciences},
genre = {Masters thesis},
year = {2024},
url = {https://nva.sikt.no/registration/01990a1b88b0-2977aaf1-0465-4e55-accd-b22aa2f8fabd}
}
@thesis{EliasHartmanTageAndersenMSc,
author = {E.~Hartman and T.~Andersen},
title = {Runtime Verification of Autonomous Robotic Systems in ROS 2},
publisher = {Norwegian University of Life Sciences},
genre = {Masters thesis},
year = {2024}
}
@thesis{Attala2023,
author = {Z.~Attala},
title = {Verification of RoboChart Models with Neural Network Components},
publisher = {University of York},
year = {2023},
genre = {PhD thesis},
url = {https://etheses.whiterose.ac.uk/id/eprint/34282/}
}
@thesis{WB2022,
author = {W.~Barnett},
title = {RoboArch: Architectural Modelling for Robotic Applications},
school = {University of York},
genre = {PhD thesis},
publisher = {University of York},
year = {2022},
url = {https://etheses.whiterose.ac.uk/id/eprint/32758/}
}
@thesis{MartinSirevågRabahSalehHagag,
author = {M.~Sirevåg and R.~S.~Hagag},
title = {Safety assurance of high voltage control module in a robotic paint system},
publisher = {University of Agder},
genre = {Masters thesis},
year = {2020}
}
@thesis{Acharjee,
author = {K.~Acharjee},
title = {Model-Based Testing of AI-Enabled Robots Applied to Nuclear Decommissioning},
publisher = {University of York},
genre = {PhD in progress}
}
@thesis{HollyHendry,
author = {H.~Hendry},
title = {Human-Robot Interaction in the Design and Verification of Robotic Systems},
publisher = {University of York},
genre = {PhD in progress}
}
@thesis{ArjunBadyal,
author = {A.~Badyal},
title = {Physics Engines for Verification of Robotic Systems},
publisher = {University of York},
genre = {PhD in progress}
}
@thesis{MustafaAdam,
author = {M.~Adam},
title = {Bridging the reality-gap: An integrated formal verification framework for RAS},
publisher = {Norwegian University of Life Sciences},
genre = {PhD in progress}
}
@thesis{YvonneMurray,
author = {Y.~Murray},
title = {Formal Verification of Industrial Robotic Systems},
publisher = {University of Agder},
genre = {PhD in progress}
}
@thesis{EliasHartmanPhD,
author = {E.~Hartman},
title = {Generative Runtime Verification of Autonomous Robotic Systems in ROS 2},
publisher = {Norwegian University of Life Sciences},
genre = {PhD in progress}
}
@techreport{RoboWorld,
title = {{R}obo{W}orld {R}eference {M}anual},
author = {J.~Baxter and G.~Carvalho and A.~Cavalcanti and S.~Ahmadi and F.~Rodrigues~J\'unior},
institution = {University of York},
year = {2023},
month = feb,
type = {{T}echnical report},
url = {https://robostar.cs.york.ac.uk/publications/techreports/reports/roboworld-reference.pdf}
}
@techreport{BCGH22,
author = {J.~Baxter and A.~Cavalcanti and M.~Gazda and R.~M.~Hierons},
institution = {University of York},
title = {Testing using {CSP} models: time, inputs, and outputs},
year = {2022},
url = {https://robostar.cs.york.ac.uk/publications/reports/BCGH22.pdf}
}
@techreport{RoboSim-Physical,
title = {{R}obo{S}im {P}hysical {M}odelling {R}eference {M}anual},
author = {A.~Miyazawa and A.~Cavalcanti and S.~Ahmadi and M.~Post and J.~Timmis},
institution = {University of York},
year = {2020},
month = nov,
type = {{T}echnical report},
url = {https://www.cs.york.ac.uk/circus/publications/techreports/reports/physmod-reference.pdf}
}
In this report, we describe a UML-like notation calledRoboSim, designedspecifically for simulation of autonomous and mobile robots, and includingtimed primitives. We provide a reference manual forRoboSim. We describethe syntax, the well-formedness conditions and semantics ofRoboSim. Wealso present three case studies and show how we can useRoboSimmodelsto check if a simulation is consistent with a functional design written in aUML-like notation.
@techreport{RoboSim,
title = {{R}obo{S}im {R}eference {M}anual},
author = {A.~Cavalcanti and P.~Ribeiro and A.~Miyazawa and A.~Sampaio and M.~Conserva~Filho and A.~Didier},
institution = {University of York},
year = {2019},
month = mar,
type = {{T}echnical report},
url = {https://robostar.cs.york.ac.uk/publications/techreports/reports/robosim-reference.pdf}
}
Autonomous and mobile robots are becoming ubiquitous. From domestic robotic vacuum cleaners to driverless cars, such robots interact with their environment and humans, leading to potential safety hazards. We propose a three-pronged solution to the problem of safety of mobile and autonomous robots: (1) domain-specific modelling with a formal underpinning; (2) automatic generation of sound simulations; and (3) verification based on model checking and theorem proving. Here, we report on a UML-like notation called RoboChart, designed specifically for modelling autonomous and mobile robots, and including timed and probabilistic primitives. We discuss a denotational semantics for a core subset of RoboChart, an approach for the development of sound simulations, and an implementation of RoboChart and its formal semantics as an Eclipse plugin supported by the CSP model checker FDR. This report is a reference manual for the RoboChart notation. It describes the syntax of RoboChart and its extensions, as well as the well-formedness conditions and semantics of the language constructs. Additionally, usage of the language is discussed via a application programming interface (API), simulation support and a number of examples.
@techreport{RoboChart,
title = {{R}obo{C}hart {R}eference {M}anual},
author = {A.~Miyazawa and A.~Cavalcanti and P.~Ribeiro and W.~Li and J.~Woodcock and J.~Timmis},
institution = {University of York},
year = {2016},
month = feb,
type = {{T}echnical report},
url = {https://www.cs.york.ac.uk/circus/publications/techreports/reports/robochart-reference.pdf}
}
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements