@article{GetirYaman2024,
title = {Specification, validation and verification of {S}ocial, {L}egal, {E}thical, {E}mpathetic and {C}ultural requirements for autonomous agents},
journal = {Journal of Systems and Software},
volume = {220},
pages = {112229},
year = {2025},
issn = {0164-1212},
doi = {10.1016/j.jss.2024.112229},
author = {S.~{Getir Yaman} and P.~Ribeiro and A.~Cavalcanti and R.~Calinescu and C.~Paterson and B.~Townsend}
}
@article{LiRMRCAWT24,
author = {Li, Wei and Ribeiro, Pedro and Miyazawa, Alvaro and Redpath, Richard and Cavalcanti, Ana and Alden, Kieran and Woodcock, Jim and Timmis, Jon},
title = {Formal design, verification and implementation of robotic controller
software via RoboChart and RoboTool},
journal = {Auton. Robots},
volume = {48},
number = {6-7},
pages = {14},
year = {2024},
doi = {10.1007/S10514-024-10163-7}
}
@article{GETIRYAMAN2024103118,
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 = {0.1016/j.scico.2024.103118},
url = {https://www.sciencedirect.com/science/article/pii/S0167642324000418},
author = {{Getir Yaman}, Sinem and Ribeiro, Pedro and Burholt, Charlie and Jones, Maddie and Cavalcanti, Ana and Calinescu, Radu}
}
@article{CavalcantiFRS24,
author = {Cavalcanti, Ana and Filho, Madiel Conserva and Ribeiro, Pedro and Sampaio, Augusto},
title = {Laws of Timed State Machines},
journal = {Comput. J.},
volume = {67},
number = {6},
pages = {2066--2107},
year = {2024},
doi = {10.1093/COMJNL/BXAD124}
}
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)}
}
@article{BaxterRC22,
author = {J.~Baxter and P.~Ribeiro and A.~Cavalcanti},
title = {Sound reasoning in tock-{CSP}},
journal = {Acta Informatica},
volume = {59},
number = {1},
pages = {125--162},
year = {2022},
doi = {10.1007/s00236-020-00394-3},
timestamp = {Fri, 13 May 2022 19:52:33 +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}
}
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}
}
@article{DBLP:journals/tcs/RibeiroC19,
author = {Ribeiro, Pedro and Cavalcanti, Ana},
title = {Angelic processes for {CSP} via the {UTP}},
journal = {Theor. Comput. Sci.},
volume = {756},
pages = {19--63},
year = {2019},
url = {https://doi.org/10.1016/j.tcs.2018.10.008},
doi = {10.1016/J.TCS.2018.10.008},
timestamp = {Sat, 09 Apr 2022 12:27:44 +0200},
biburl = {https://dblp.org/rec/journals/tcs/RibeiroC19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{ShaukatDKBMRARD24,
author = {Shaukat, Nabil and Dubey, Shival and Kaddouh, Bilal Y. and Blight, Andy and Mudrich, Lenka and Ribeiro, Pedro and Ara{\'{u}}jo, Hugo and Richardson, Rob and Dennis, Louise Abigail and Cavalcanti, Ana Lucia Caneca and Mousavi, Mohammad},
title = {Trustworthy {ROS} Software Architecture for Autonomous Drones Missions:
From RoboChart Modelling to {ROS} Implementation},
booktitle = {20th {IEEE/ASME} International Conference on Mechatronic and Embedded
Systems and Applications, {MESA} 2024, Genova, Italy, September 2-4,
2024},
pages = {1--7},
publisher = {{IEEE}},
year = {2024},
doi = {10.1109/MESA61532.2024.10704818}
}
@inproceedings{CavalcantiI2021,
author = {Cavalcanti, Ana and Attala, Ziggy and Baxter, James and Miyazawa, Alvaro and Ribeiro, Pedro},
editor = {Cerone, Antonio},
title = {Model-Based Engineering for Robotics with RoboChart and RoboTool},
booktitle = {Formal Methods for an Informal World - {ICTAC} 2021 Summer School,
Virtual Event, Astana, Kazakhstan, September 1-7, 2021, Tutorial Lectures},
series = {Lecture Notes in Computer Science},
volume = {13490},
pages = {106--151},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-031-43678-9\_4},
doi = {10.1007/978-3-031-43678-9\_4}
}
@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{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}
}
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}
}
@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}
}
@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}
}
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 = {Ribeiro, P. and Cavalcanti, A. and Woodcock, J.},
booktitle = {{U}nifying {T}heories of {P}rogramming},
publisher = {Springer International Publishing},
year = {2016},
note = {(to appear)},
series = {{L}ecture {N}otes in {C}omputer {S}cience},
owner = {wv8579},
timestamp = {2016.08.09}
}
@inproceedings{LiM0CWT16,
author = {W.~Li and A.~Miyazawa and P.~Ribeiro and A.~Cavalcanti and J.~Woodcock and J.~Timmis},
editor = {R.~Gro{\ss} and A.~Kolling and S.~Berman and E.~Frazzoli and A.~Martinoli and F.~Matsuno and M.~Gauci},
title = {From Formalised State Machines to Implementations of Robotic Controllers},
booktitle = {Distributed Autonomous Robotic Systems, The 13th International Symposium,
{DARS} 2016, Natural History Museum, London, UK, November 7-9, 2016},
series = {Springer Proceedings in Advanced Robotics},
volume = {6},
pages = {517--529},
publisher = {Springer},
year = {2016},
doi = {10.1007/978-3-319-73008-0\_36}
}
The concept of angelic nondeterminism has traditionally been employed in the refinement calculus. Despite different notions having been proposed in the context of process algebras, namely Communicating Sequential Processes (CSP), the analogous counterpart to the angelic choice operator of the monotonic predicate transformers, has been elusive. In order to consider this concept in the context of reactive processes, we introduce a new theory in the setting of Hoare and He’s Unifying Theories of Programming (UTP). Based on a theory of designs with angelic nondeterminism previously developed, we show how these processes can be similarly expressed as reactive designs. Furthermore, a Galois connection is established with the existing theory of reactive processes and a bijection is also found with respect to the subset of non-angelic processes.
@incollection{Ribeiro2014,
title = {{A}ngelicism in the {T}heory of {R}eactive {P}rocesses},
author = {Ribeiro, Pedro and Cavalcanti, Ana},
booktitle = {{U}nifying {T}heories of {P}rogramming},
publisher = {Springer International Publishing},
year = {2015},
editor = {Naumann, David},
pages = {42-61},
series = {{L}ecture {N}otes in {C}omputer {S}cience},
volume = {8963},
doi = {10.1007/978-3-319-14806-9_3},
isbn = {978-3-642-35704-6},
owner = {pfr500},
timestamp = {2014.06.05}
}
The total correctness of sequential computations can be established through different isomorphic models, such as monotonic predicate transformers and binary multirelations, where both angelic and demonic nondeterminism are captured. Assertional models can also be used to characterise process algebras: in Hoare and He’s Unifying Theories of Programming, CSP processes can be specified as the range of a healthiness condition over designs, which are pre and postcondition pairs. In this context, we have previously developed a theory of angelic designs that is a stepping stone for the natural extension of the concept of angelic nondeterminism to the theory of CSP. In this paper we present an extended model of upward-closed binary multirelations that is isomorphic to angelic designs. This is a richer model than that of standard binary multirelations, in that we admit preconditions that rely on later or final observations as required for a treatment of processes.
@incollection{Ribeiro2014a,
title = {{UTP} {D}esigns for {B}inary {M}ultirelations},
author = {Ribeiro, Pedro and Cavalcanti, Ana},
booktitle = {{T}heoretical {A}spects of {C}omputing {ICTAC} 2014},
publisher = {Springer International Publishing},
year = {2014},
editor = {Ciobanu, Gabriel and M\'{e}ry, Dominique},
pages = {388-405},
series = {{L}ecture {N}otes in {C}omputer {S}cience},
volume = {8687},
doi = {10.1007/978-3-319-10882-7_23},
isbn = {978-3-642-39717-2},
owner = {pfr500},
timestamp = {2014.07.04}
}
Hoare and He’s Unifying Theories of Programming (UTP) are a predicative relational framework for the definition and combination of refinement languages for a variety of programming paradigms. Previous work has defined a theory for angelic nondeterminism in the UTP; this is basically an encoding of binary multirelations in a predicative model. In the UTP a theory of designs (pre and postcondition pairs) provides, not only a model of terminating programs, but also a stepping stone to define a theory for state-rich reactive processes. In this paper, we cast the angelic nondeterminism theory of the UTP as a theory of designs with the long-term objective of providing a model for well established refinement process algebras like Communicating Sequential Processes (CSP) and Circus.
@inproceedings{Ribeiro2013,
title = {{D}esigns with {A}ngelic {N}ondeterminism},
author = {Ribeiro, P. and Cavalcanti, A.},
booktitle = {{T}heoretical {A}spects of {S}oftware {E}ngineering ({TASE}), 2013 {I}nternational {S}ymposium on},
year = {2013},
pages = {71-78},
publisher = {IEEE},
doi = {10.1109/TASE.2013.18},
keywords = {communicating sequential processes;formal specification;program verification;refinement calculus;relational algebra;CSP;Circus;UTP;Unifying Theories of Programming;angelic nondeterminism theory;binary multirelation encoding;communicating sequential process;predicative model;predicative relational framework;program termination;programming paradigm;refinement language;refinement process algebra;state-rich reactive process;Algebra;Educational institutions;Electronic mail;Encoding;Lattices;Programming},
owner = {pfr},
timestamp = {2013.12.06}
}
@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.cs.york.ac.uk/%7Ealcc/publications/papers/CBBCFMRS21.pdf}
}
@article{CavalcantiR20,
author = {A.~Cavalcanti and P.~Ribeiro},
title = {Editorial},
journal = {Formal Aspects Comput.},
volume = {32},
number = {2-3},
pages = {155},
year = {2020},
doi = {10.1007/s00165-020-00516-1},
keywords = {editorial}
}
@proceedings{UTP2019,
editor = {P.~Ribeiro and A.~Sampaio},
title = {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},
series = {Lecture Notes in Computer Science},
volume = {11885},
publisher = {Springer},
year = {2019},
doi = {10.1007/978-3-030-31038-7},
isbn = {978-3-030-31037-0},
keywords = {editorial}
}
@article{FosterZNRW19,
author = {S.~Foster and F.~Zeyda and Y.~Nemouchi and P.~Ribeiro and B.~Wolff},
title = {Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories
of Programming},
journal = {Arch. Formal Proofs},
volume = {2019},
year = {2019},
url = {https://www.isa-afp.org/entries/UTP.html},
timestamp = {Thu, 21 Jan 2021 17:34:51 +0100},
keywords = {afp}
}
@techreport{Ribeiro2016a,
title = {{S}uper-{T}heories},
author = {Ribeiro, Pedro},
institution = {University of York},
year = {2016},
note = {\url{https://www-users.cs.york.ac.uk/pfr/reports/super-theories.pdf}},
owner = {wv8579},
timestamp = {2016.03.08},
url = {https://www-users.cs.york.ac.uk/pfr/reports/super-theories.pdf}
}
@techreport{Ribeiro2013a,
title = {{R}eactive angelic processes},
author = {Ribeiro, Pedro},
institution = {University of York},
year = {2014},
month = feb,
note = {http://www-users.cs.york.ac.uk/pfr/reports/rac.pdf},
type = {{T}echnical report},
owner = {pfr500},
timestamp = {2013.12.12},
url = {http://www-users.cs.york.ac.uk/pfr/reports/rac.pdf}
}
@techreport{Ribeiro2013b,
title = {{D}esigns with {A}ngelic {N}ondeterminism},
author = {Ribeiro, Pedro},
institution = {University of York},
year = {2013},
month = feb,
note = {http://www-users.cs.york.ac.uk/pfr/reports/dac.pdf},
type = {{T}echnical {R}eport},
owner = {pfr},
timestamp = {2013.02.07},
url = {http://www-users.cs.york.ac.uk/pfr/reports/dac.pdf}
}
@phdthesis{RibeiroT2014,
title = {{A}ngelic {P}rocesses},
author = {Ribeiro, P.},
school = {University of York},
year = {2014},
month = dec,
type = {{P}h.{D}. dissertation (extended version)},
owner = {pfr500},
timestamp = {2014.11.05},
url = {http://arxiv.org/abs/1505.04726}
}
@phdthesis{RibeiroT2014b,
title = {{A}ngelic {P}rocesses},
author = {Ribeiro, P.},
school = {University of York},
year = {2014},
month = dec,
note = {http://etheses.whiterose.ac.uk/9020/},
type = {{Ph.D} thesis},
owner = {wv8579},
timestamp = {2015.07.26},
url = {http://etheses.whiterose.ac.uk/9020/}
}