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}
}
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{Ribeiro2018,
title = {Angelic Processes for {CSP} via the {UTP}},
journal = {Theoretical Computer Science},
year = {2018},
issn = {0304-3975},
doi = {10.1016/j.tcs.2018.10.008},
url = {http://www.sciencedirect.com/science/article/pii/S0304397518306133},
author = {Ribeiro, Pedro and Cavalcanti, Ana},
keywords = {Semantics, formal specification, process algebras, CSP, UTP}
}
@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{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}
}
@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{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}
}
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}
}
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/}
}