Department of Computer Science

Publications

  • 1. K. Ye, S. Foster, J. Woodcock: Formally verified animation for RoboChart using interaction trees. Journal of Logical and Algebraic Methods in Programming. 137, 100940 (2024).

    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}
    }
    
  • 2. A. Cavalcanti, M. C. Filho, P. Ribeiro, A. Sampaio: Laws of Timed State Machines. The Computer Journal. bxad124 (2023).

    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}
    }
    
  • 3. J. Baxter, G. Carvalho, A. Cavalcanti, F. R. Júnior: RoboWorld: Verification of Robotic Systems with Environment in the Loop. Form. Asp. Comput. 35, (2023).

    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}
    }
    
  • 4. Z. Attala, A. Cavalcanti, J. Woodcock: Modelling and Verifying Robotic Software that Uses Neural Networks. In: Ábrahám, E. et al. (eds.) Theoretical Aspects of Computing – ICTAC 2023. pp. 15–35. Springer (2023).

    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}
    }
    
  • 5. J. Woodcock, A. Cavalcanti, S. Foster, M. Oliveira, A. Sampaio, F. Zeyda: UTP, Circus, and Isabelle. In: Bowen, J.P. et al. (eds.) Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday. pp. 19–51. Springer Nature Switzerland, Cham (2023).

    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}
    }
    
  • 6. M. Adam, K. Ye, D. A. Anisi, A. Cavalcanti, J. Woodcock, R. Morris: Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment. In: 2023 IEEE 19th International Conference on Automation Science and Engineering (CASE). pp. 1–7 (2023).
    @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}
    }
    
  • 7. A. Cavalcanti, A. Miyazawa, U. Schulze, J. Timmis: Bringing RoboStar and RT-Tester Together. In: Haxthausen, A.E. et al. (eds.) Applicable Formal Methods for Safe Industrial Products: Essays Dedicated to Jan Peleska on the Occasion of His 65th Birthday. pp. 16–33. Springer Nature Switzerland, Cham (2023).

    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}
    }
    
  • 8. H. Hendry, M. Chattington, A. Cavalcanti, C. McCall: Verification of a search-and-rescue drone with humans in the loop. In: Ahram, T. and Karwowski, W. (eds.) Human Factors in Robots, Drones and Unmanned Systems. AHFE (2023) International Conference. AHFE International, USA (2023).
    @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}
    }
    
  • 9. A. Cavalcanti, R. M. Hierons: Challenges in testing of cyclic systems. In: 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS). pp. 1–6 (2023).
    @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}
    }
    
  • 10. M. R. Mousavi, A. Cavalcanti, M. Fisher, L. A. Dennis, R. M. Hierons, B. Y. Kaddouh, E. L.-C. Law, R. C. Richardson, J. O. Ringer, I. Tyukin, J. Woodcock: Trustworthy Autonomous Systems Through Verifiability. Computer. 56, 40–47 (2023).
    @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}
    }
    
  • 11. J. Baxter, A. Cavalcanti, M. Gazda, R. M. Hierons: Testing using CSP Models: Time, Inputs, and Outputs. ACM Trans. Comput. Log. 24, 17:1–17:40 (2023).
    @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}
    }
    
  • 12. S. G. Yaman, C. Burholt, M. Jones, R. Calinescu, A. Cavalcanti: Specification and Validation of Normative Rules for Autonomous Agents. In: Lambers, L. and Uchitel, S. (eds.) 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. pp. 241–248. Springer (2023).
    @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}
    }
    
  • 13. K. Ye, A. Cavalcanti, S. Foster, A. Miyazawa, J. Woodcock: Probabilistic modelling and verification using RoboChart and PRISM. Software and Systems Modeling. 21, 667–716 (2022).
    @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}
    }
    
  • 14. B. Townsend, C. Paterson, T. T. Arvind, G. Nemirovsky, R. Calinescu, A. Cavalcanti, I. Habli, A. Thomas: From Pluralistic Normative Principles to Autonomous-Agent Rules. Minds Mach. 32, 683–715 (2022).
    @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}
    }
    
  • 15. W. Barnett, A. Cavalcanti, A. Miyazawa: Architectural modelling for robotics: RoboArch and the CorteX example. Frontiers Robotics AI. 9, (2022).
    @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}
    }
    
  • 16. T. Kulik, B. Dongol, P. G. Larsen, H. D. Macedo, S. Schneider, P. W. V. Tran-Jørgensen, J. Woodcock: A Survey of Practical Formal Methods for Security. Formal Aspects of Computing. 34, 1–39 (2022).
    @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}
    }
    
  • 17. M. Windsor, A. Cavalcanti: RoboCert: Property Specification in Robotics. In: A. Riesco and M. Zhang (eds.) Formal Methods and Software Engineering. pp. 386–403. Springer (2022).

    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}
    }
    
  • 18. K. Ye, S. Foster, J. Woodcock: Formally Verified Animation for RoboChart Using Interaction Trees. In: A. Riesco and M. Zhang (eds.) Formal Methods and Software Engineering. pp. 404–420. Springer (2022).

    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}
    }
    
  • 19. F. Yan, S. Foster, I. Habli, R. Wei: Model-based Generation of Hazard-driven Arguments and Formal Verification Evidence for Assurance Cases. In: L. F. Pires et al. (eds.) Proceedings of the 10th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2022, Online Streaming, February 6-8, 2022. pp. 252–263. SCITEPRESS (2022).
    @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}
    }
    
  • 20. Y. Murray, M. Sirevåg, P. Ribeiro, D. A. Anisi, M. Mossige: Safety assurance of an industrial robotic control system using hardware/software co-verification. Science of Computer Programming. (2022).

    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)}
    }
    
  • 21. J. S. Fitzgerald, P. G. Larsen, T. Margaria, J. Woodcock, C. Gomes: Engineering of Digital Twins for Cyber-Physical Systems. In: T. Margaria and B. Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Practice - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part IV. pp. 3–8. Springer (2022).
    @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}
    }
    
  • 22. T. Wright, C. Gomes, J. Woodcock: Formally Verified Self-adaptation of an Incubator Digital Twin. In: T. Margaria and B. Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Practice - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part IV. pp. 89–109. Springer (2022).
    @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}
    }
    
  • 23. B. Townsend, C. Paterson, T. T. Arvind, G. Nemirovsky, R. Calinescu, A. Cavalcanti, I. Habli, A. Thomas: From Pluralistic Normative Principles to Autonomous-Agent Rules. Minds Mach. 32, 683–715 (2022).
    @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}
    }
    
  • 24. D. Du, A. Cavalcanti, J. Nie: RoboSimVer: A Tool for RoboSim Modeling and Analysis. In: 37th IEEE/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, October 10-14, 2022. pp. 164:1–164:4. ACM (2022).
    @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}
    }
    
  • 25. J. Baxter, P. Ribeiro, A. Cavalcanti: Sound reasoning in tock-CSP. Acta Informatica. (2021).
    @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}
    }
    
  • 26. W. Lindoso, S. C. Nogueira, R. Domingues, L. Lima: Visual Specification of Properties for Robotic Designs. In: S. Campos and M. Minea (eds.) Formal Methods: Foundations and Applications - 24th Brazilian Symposium, SBMF 2021, Virtual Event, December 6-10, 2021, Proceedings. pp. 34–52. Springer (2021).
    @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}
    }
    
  • 27. S. Foster, Y. Nemouchi, M. Gleirscher, R. Wei, T. Kelly: Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM. Formal Aspects Comput. 33, 855–884 (2021).
    @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}
    }
    
  • 28. A. Walter, S. J. Bale, A. Tyrrell: Implementation of Reduced Precision Integer Epigenetic Networks in Hardware. In: IEEE SSCI 2021 (Symposium Series on Computational Intelligence). IEEE (2021).
    @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/}
    }
    
  • 29. A. Cavalcanti, J. Baxter, G. Carvalho: RoboWorld: Where Can My Robot Work? In: R. Calinescu and C. S. Pasareanu (eds.) Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings. pp. 3–22. Springer (2021).
    @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}
    }
    
  • 30. A. Abba, A. Cavalcanti, J. Jacob: Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata. In: S. Campos and M. Minea (eds.) Formal Methods: Foundations and Applications - 24th Brazilian Symposium, SBMF 2021, Virtual Event, December 6-10, 2021, Proceedings. pp. 70–86. Springer (2021).
    @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}
    }
    
  • 31. K. Ye, S. Foster, J. Woodcock: Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving. In: U. Fahrenberg et al. (eds.) Relational and Algebraic Methods in Computer Science. pp. 465–482. Springer International Publishing (2021).

    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}
    }
    
  • 32. M. Gleirscher, R. Calinescu, J. Woodcock: RiskStructures: A design algebra for risk-aware machines. Formal Aspects Computing. 33, 763–802 (2021).
    @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}
    }
    
  • 33. L. Esterle, B. Porter, J. Woodcock: Verification and Uncertainties in Self-integrating System. In: E. El-Araby et al. (eds.) IEEE International Conference on Autonomic Computing and Self-Organizing Systems, ACSOS 2021, Companion Volume, Washington, DC, USA, September 27 - Oct. 1, 2021. pp. 220–225. IEEE (2021).
    @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}
    }
    
  • 34. J. Woodcock: Hoare and He’s Unifying Theories of Programming. In: Theories of Programming: The Life and Works of Tony Hoare. pp. 285–316. Association for Computing Machinery, New York, NY, USA (2021).
    @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}
    }
    
  • 35. M. Zhang, D. Du, A. C. A. Sampaio, A. L. C. Cavalcanti, Filho, M.C., M. Zhang: Transforming RoboSim Models into UPPAAL. In: 15th International Symposium on Theoretical Aspects of Software Engineering. pp. 71–78. IEEE (2021).
    @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}
    }
    
  • 36. A. L. C. Cavalcanti: RoboStar Modelling Stack: Tackling the Reality Gap. In: 1st International Workshop on Verification of Autonomous & Robotic Systems. Association for Computing Machinery (2021).
    @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}
    }
    
  • 37. A. L. C. Cavalcanti, B. Dongol, R. Hierons, J. Timmis, J. C. P. Woodcock eds: Software Engineering for Robotics. Springer International Publishing (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}
    }
    
  • 38. A. L. C. Cavalcanti, W. Barnett, J. Baxter, G. Carvalho, M. C. Filho, A. Miyazawa, P. Ribeiro, A. C. A. Sampaio: RoboStar Technology: A Roboticist’s Toolbox for Combined Proof, Simulation, and Testing. In: A. L. C. Cavalcanti et al. (eds.) Software Engineering for Robotics. pp. 249–293. Springer International Publishing (2021).
    @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}
    }
    
  • 39. X. Chen, Z. Liu, J. Wang, J. Woodcock: Editorial. Formal Aspects Comput. 33, 299–300 (2021).
    @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}
    }
    
  • 40. H. Zhao, X. Zeng, T. Chen, Z. Liu, J. Woodcock: Learning safe neural network controllers with barrier certificates. Formal Aspects Comput. 33, 437–455 (2021).
    @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}
    }
    
  • 41. E. P. de Vink, A. Cavalcanti: Editorial. Formal Aspects Comput. 33, 1–2 (2021).
    @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}
    }
    
  • 42. S. Foster, K. Ye, A. Cavalcanti, J. Woodcock: Automated verification of reactive and concurrent programs by calculation. J. Log. Algebraic Methods Program. 121, 100681 (2021).
    @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}
    }
    
  • 43. Z. Attala, A. L. C. Cavalcanti, J. C. P. Woodcock: A Comparison of Neural Network Tools for the Verification of Linear Specifications of ReLU Networks. In: A. Albarghouthi et al. (eds.) 3rd Workshop on Formal Methods for ML-Enabled Autonomous System. pp. 22–33 (2020).
    @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}
    }
    
  • 44. T. Lecomte, D. Déharbe, P. Fournier, M. Oliveira: The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199, 102524 (2020).
    @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}
    }
    
  • 45. W. Chang, R. Wei, S. Zhao, A. J. Wellings, J. Woodcock, A. Burns: Development Automation of Real-Time Java: Model-Driven Transformation and Synthesis. ACM Trans. Embed. Comput. Syst. 19, 31:1–31:26 (2020).
    @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}
    }
    
  • 46. A. Cavalcanti, Hierons, R.M., Nogueira, S.C.: Inputs and Outputs in CSP: A Model and a Testing Theory. ACM Trans. Comput. Log. 21, 24:1–24:53 (2020).
    @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}
    }
    
  • 47. A. Cavalcanti: Modelling and Verification of Robotic Platforms for Simulation Using RoboStar Technology. In: Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings. pp. 3–5 (2020).
    @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}
    }
    
  • 48. S. Foster, J. Baxter, A. Cavalcanti, J. Woodcock, F. Zeyda: Unifying semantic foundations for automated verification tools in Isabelle/UTP. Sci. Comput. Program. 197, 102510 (2020).
    @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}
    }
    
  • 49. K. Ye, S. Foster, J. Woodcock: Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP. In: Adamatzky, A. and Kendon, V. (eds.) From Astrophysics to Unconventional Computation: Essays Presented to Susan Stepney on the Occasion of her 60th Birthday. pp. 215–254. Springer International Publishing (2020).

    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}
    }
    
  • 50. S. Foster, Y. Nemouchi, C. O’Halloran, K. Stephenson, N. Tudor: Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study. In: FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, July 13, 2020. pp. 11–21 (2020).
    @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}
    }
    
  • 51. Y. Murray, D. A. Anisi, M. Sirevåg, P. Ribeiro, R.S. Hagag: Safety Assurance of a High Voltage Controller for an Industrial Robotic System. In: Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings. pp. 45–63 (2020).
    @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}
    }
    
  • 52. S. Foster, J. J. Huerta y Munive, G. Struth: Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL. In: Relational and Algebraic Methods in Computer Science - 18th International Conference, RAMiCS 2020, Palaiseau, France, April 8-11, 2020, Proceedings . pp. 169–186 (2020).
    @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}
    }
    
  • 53. S. Foster, J. Baxter: Automated Algebraic Reasoning for Collections and Local Variables with Lenses. In: Relational and Algebraic Methods in Computer Science - 18th International Conference, RAMiCS 2020, Palaiseau, France, April 8-11, 2020, Proceedings . pp. 100–116 (2020).
    @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}
    }
    
  • 54. M. Gleirscher, S. Foster, J. C. P. Woodcock: New Opportunities for Integrated Formal Methods. ACM Comput. Surv. 52, 117:1–117:36 (2020).
    @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}
    }
    
  • 55. S. Foster, A. L. C. Cavalcanti, S. Canham, J. C. P. Woodcock, Zeyda, F.: Unifying theories of reactive design contracts. Theor. Comput. Sci. 802, 105–140 (2020).
    @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}
    }
    
  • 56. P. Ribeiro: A Unary Semigroup Trace Algebra. In: Relational and Algebraic Methods in Computer Science - 18th International Conference, RAMiCS 2020, Palaiseau, France, April 8-11, 2020, Proceedings . pp. 270–285 (2020).
    @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}
    }
    
  • 57. A. Miyazawa, P. Ribeiro, L. Wei, A. L. C. Cavalcanti, J. Timmis, J. C. P. Woodcock: RoboChart: modelling and verification of the functional behaviour of robotic applications. Software & Systems Modeling. 18, 3097–3149 (2019).

    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}
    }
    
  • 58. Y. Nemouchi, S. Foster, M. Gleirscher, T. Kelly: Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. In: Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. pp. 379–398 (2019).
    @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}
    }
    
  • 59. M. Gleirscher, S. Foster, Y. Nemouchi: Evolution of Formal Model-Based Assurance Cases for Autonomous Robots. In: Software Engineering and Formal Methods - 17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings. pp. 87–104 (2019).
    @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}
    }
    
  • 60. J. Woodcock, A. Cavalcanti, S. Foster, A. Mota, K. Ye: Probabilistic Semantics for RoboChart - A Weakest Completion Approach. In: 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. pp. 80–105 (2019).
    @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}
    }
    
  • 61. S. Foster: Hybrid Relations in Isabelle/UTP. In: 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. pp. 130–153 (2019).
    @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}
    }
    
  • 62. J. Peleska, W. Huang, A. Cavalcanti: Finite complete suites for CSP refinement testing. Sci. Comput. Program. 179, 1–23 (2019).
    @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}
    }
    
  • 63. A. Cavalcanti, J. Baxter, R. M. Hierons, R. Lefticaru: Testing Robots Using CSP. In: 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. pp. 21–38 (2019).
    @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}
    }
    
  • 64. T. Hoare, G. Struth, J. Woodcock: A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic. In: 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. pp. 3–21 (2019).
    @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}
    }
    
  • 65. P. Ribeiro, A. L. C. Cavalcanti: Angelic processes for CSP via the UTP. Theoretical Computer Science. 756, 19–63 (2019).

    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}
    }
    
  • 66. A. Miyazawa, A. L. C. Cavalcanti, A. Wellings: SCJ-Circus: specification and refinement of Safety-Critical Java programs. Science of Computer Programming. (2019).

    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}
    }
    
  • 67. A. L. C. Cavalcanti, A. C. A. Sampaio, A. Miyazawa, P. Ribeiro, M. S. Conserva Filho, A. Didier, W. Li, J. Timmis: Verified simulation for robotics. Science of Computer Programming. 174, 1–37 (2019).

    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}
    }
    
  • 68. S. Foster, A. L. C. Cavalcanti, J. C. P. Woodcock, F. Zeyda: Unifying theories of time with generalised reactive processes . Information Processing Letters. 135, 47–52 (2018).

    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}
    }
    
  • 69. M. S. Conserva Filho, M. V. M. Oliveira, A. C. A. Sampaio, A. L. C. Cavalcanti: Compositional and Local Livelock Analysis for CSP. Information Processing Letters. 133, 21–25 (2018).

    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}
    }
    
  • 70. S. Foster, J. Baxter, A. L. C. Cavalcanti, A. Miyazawa, J. C. P. Woodcock: Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. In: Formal Aspects of Component Software. pp. 137–155. Springer International Publishing, Cham (2018).
    @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}
    }
    
  • 71. A. L. C. Cavalcanti, A. Miyazawa, A. C. A. Sampaio, W. Li, P. Ribeiro, J. Timmis: Modelling and Verification for Swarm Robotics. In: Integrated Formal Methods. pp. 1–19. Springer International Publishing, Cham (2018).

    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}
    }
    
  • 72. S. Foster, K. Ye, A. L. C. Cavalcanti, J. C. P. Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. In: Relational and Algebraic Methods in Computer Science. pp. 205–224. Springer International Publishing, Cham (2018).

    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}
    }
    
  • 73. F. Zeyda, J. Ouy, S. Foster, A. L. C. Cavalcanti: Formalising Cosimulation Models. In: A. Cerone and M. Roveri (eds.) Software Engineering and Formal Methods - SEFM 2017 Collocated Workshops. pp. 453–468. Springer (2018).

    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}
    }
    
  • 74. W. Li, A. Miyazawa, P. Ribeiro, A. L. C. Cavalcanti, J. C. P. Woodcock, J. Timmis: From formalised state machines to implementation of robotic controllers. In: Groß, R. et al. (eds.) Distributed Autonomous Robotic Systems: The 13th International Symposium. pp. 517–529. Springer International Publishing (2018).

    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}
    }
    
  • 75. Conserva Filho, M.S., Marinho, R., Mota, A., Woodcock, J.: Analysing RoboChart with Probabilities. In: Massoni, T. and Mousavi, M.R. (eds.) Formal Methods: Foundations and Applications. pp. 198–214. Springer International Publishing, Cham (2018).

    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}
    }
    
  • 76. A. L. C. Cavalcanti, A. Miyazawa, R. Payne, J. Woodcock: Sound Simulation and Co-simulation for Robotics. In: M. Mazzara and B. Meyer (eds.) Present and Ulterior Software Engineering. pp. 173–194. Springer International Publishing (2017).

    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}
    }
    
  • 77. R. Otoni, A. L. C. Cavalcanti, A. C. A. Sampaio: Local Analysis of Determinism for CSP. In: S. Cavalheiro and J. Fiadeiro (eds.) Formal Methods: Foundations and Applications. pp. 107–124. Springer International Publishing (2017).

    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}
    }
    
  • 78. A. Miyazawa, P. Ribeiro, W. Li, A. L. C. Cavalcanti, J. Timmis: Automatic Property Checking of Robotic Applications. In: The International Conference on Intelligent Robots and Systems. pp. 3869–3876 (2017).

    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}
    }
    
  • 79. P. Ribeiro, A. Miyazawa, W. Li, A. L. C. Cavalcanti, J. Timmis: Modelling and Verification of Timed Robotic Controllers. In: N. Polikarpova and S. Schneider (eds.) Integrated Formal Methods. pp. 18–33. Springer (2017).

    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}
    }
    
  • 80. A. L. C. Cavalcanti, J. C. P. Woodcock, N. Amálio: Behavioural Models for FMI Co-simulations. In: A. C. A. Sampaio and F. Wang (eds.) International Colloquium on Theoretical Aspects of Computing. Springer (2016).

    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}
    }
    
  • 81. S. Foster, B. Thiele, A. L. C. Cavalcanti, J. C. P. Woodcock: Towards a UTP semantics for Modelica. In: Unifying Theories of Programming. Springer (2016).

    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}
    }
    
  • 82. P. Ribeiro, A. L. C. Cavalcanti, J. C. P. Woodcock: A Stepwise Approach to Linking Theories. In: Unifying Theories of Programming. Springer International Publishing (2016).

    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}
    }
    

Technical Reports

  • 1. J. Baxter, G. Carvalho, A. Cavalcanti, S. Ahmadi, F. Rodrigues Júnior: RoboWorld Reference Manual. University of York (2023).
    @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}
    }
    
  • 2. J. Baxter, A. Cavalcanti, M. Gazda, R. M. Hierons: Testing using CSP models: time, inputs, and outputs. University of York (2022).
    @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}
    }
    
  • 3. A. Miyazawa, A. Cavalcanti, S. Ahmadi, M. Post, J. Timmis: RoboSim Physical Modelling Reference Manual. University of York (2020).
    @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}
    }
    
  • 4. A. Cavalcanti, P. Ribeiro, A. Miyazawa, A. Sampaio, M. Conserva Filho, A. Didier: RoboSim Reference Manual. University of York (2019).

    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}
    }
    
  • 5. A. Miyazawa, A. Cavalcanti, P. Ribeiro, W. Li, J. Woodcock, J. Timmis: RoboChart Reference Manual. University of York (2016).

    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