RoboTest: : Systematic Model-Based Testing and Simulation of Mobile Autonomous Robots
Lead Research Organisation:
University of York
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
- University of York (Lead Research Organisation)
- Technical University of Munich (Collaboration)
- University of Surrey (Collaboration)
- Thales Group (Collaboration)
- Transport Systems Catapult (Collaboration)
- Microsoft Research (Collaboration)
- University of Agder (Collaboration)
- UFPE (Collaboration)
- University of Bremen (Collaboration)
- Seoul National University (Collaboration)
- Federal University of Pernambuco (Collaboration)
- Fudan University (Collaboration)
- D-RisQ (Collaboration)
- Aarhus University (Collaboration)
- Southwest University (Collaboration)
- Technical University Berlin (Collaboration)
- Norwegian University of Life Sciences (NMBU) (Collaboration)
- Lancaster University (Collaboration)
- Galois, Inc. (Collaboration)
- Trinity College Dublin (Collaboration)
- Defence Science & Technology Laboratory (DSTL) (Collaboration)
- Simomics Ltd (Collaboration)
- Praxis Systems Ltd (Collaboration)
- Altran (Collaboration)
- East China Normal University (ECNU) (Collaboration)
- ABB Group (Collaboration)
- Indian Institute of Science Bangalore (Collaboration)
- UNIVERSITY OF YORK (Collaboration)
- KING'S COLLEGE LONDON (Collaboration)
Publications
A. Miyazawa
(2020)
RoboSim Physical Modelling Reference Manual
Alagundagi DB
(2023)
Exploring breast cancer exosomes for novel biomarkers of potential diagnostic and prognostic importance.
in 3 Biotech
Andrew Walter
(2021)
Implementation of Reduced Precision Integer Epigenetic Networks in Hardware
Barnett W
(2022)
Architectural modelling for robotics: RoboArch and the CorteX example.
in Frontiers in robotics and AI
Barnett W
(2018)
Framework for the Simulation of Robochart Models Using ROS
Baxter J
(2023)
Testing using CSP Models: Time, Inputs, and Outputs
in ACM Transactions on Computational Logic
Baxter J
(2021)
Sound reasoning in tock-CSP
in Acta Informatica
Baxter J
(2021)
Sound reasoning in tock-CSP
in Acta Informatica
Cavalcanti A
(2019)
Fault-based refinement-testing for CSP
in Software Quality Journal
Cavalcanti A
(2021)
Software Engineering for Robotics
Cavalcanti A
(2020)
Inputs and Outputs in CSP A Model and a Testing Theory
in ACM Transactions on Computational Logic
Cavalcanti A
(2019)
Verified simulation for robotics
in Science of Computer Programming
Cavalcanti A
(2020)
Editorial
in Formal Aspects of Computing
Cavalcanti A
(2021)
RoboStar modelling stack: tackling the reality gap
Chang W
(2020)
Development Automation of Real-Time Java Model-Driven Transformation and Synthesis
in ACM Transactions on Embedded Computing Systems
Chen X
(2021)
Editorial
in Formal Aspects of Computing
Chugh A
(2023)
Comparative docking studies of drugs and phytocompounds for emerging variants of SARS-CoV-2.
in 3 Biotech
Da Silva L
(2023)
Antibacterial potential of chalcones and its derivatives against Staphylococcus aureus.
in 3 Biotech
Da Silva L
(2023)
Antibacterial potential of chalcones and its derivatives against Staphylococcus aureus.
in 3 Biotech
Esterle L
(2021)
Verification and Uncertainties in Self-integrating System
Fantechi A
(2021)
Editorial
in Formal Aspects of Computing
Foster S
(2021)
Automated verification of reactive and concurrent programs by calculation
in Journal of Logical and Algebraic Methods in Programming
Foster S
(2021)
Automated verification of reactive and concurrent programs by calculation
in Journal of Logical and Algebraic Methods in Programming
Foster S
(2018)
Unifying theories of time with generalised reactive processes
in Information Processing Letters
Foster S
(2020)
Unifying semantic foundations for automated verification tools in Isabelle/UTP
in Science of Computer Programming
Gleirscher M
(2019)
New Opportunities for Integrated Formal Methods
in ACM Computing Surveys
Gleirscher M
(2021)
Proceedings First Workshop on Applicable Formal Methods Preface
in Electronic Proceedings in Theoretical Computer Science
Gleirscher M
(2021)
RiskStructures : A design algebra for risk-aware machines
in Formal Aspects of Computing
Hendry HR
(2022)
Verification of Robotic Systems with Humans in the Loop
Kulik T
(2021)
A Survey of Practical Formal Methods for Security
in ArXiv
Kulik T
(2022)
A Survey of Practical Formal Methods for Security
in Formal Aspects of Computing
Larsen P
(2018)
Software Engineering and Formal Methods
Mario Gleirscher
(2021)
EPTCS
Mishra S
(2023)
'Cyclic syndrome' of arrears and efficiency of Indian judiciary.
in SN business & economics
Miyazawa A
(2019)
RoboChart: modelling and verification of the functional behaviour of robotic applications
in Software & Systems Modeling
Mousavi M
(2023)
Trustworthy Autonomous Systems Through Verifiability
in Computer
| Description | This is the same as EP/R025134/1. |
| Exploitation Route | This is the same as EP/R025134/1. |
| Sectors | Other |
| Description | We have participated of public engagement activities to disseminate the work. We have reached out to schools, the York Festival of Ideas, and the Pint of Science. For an audience more focused on science and engineering, but still generalist, we have written popular articles, given webinars, and published a podcast. We have also developed new material for YorkTalks (https://www.york.ac.uk/research/events/yorktalks/). We have material ready and are developing more material to engage in this form of activity. As a result, we have also trained the Research Assistants in dealing with the public. We are engaging with industry nationally and internationally to train human resources and support the development of new tools. Colleagues in industry are also leading the effort. 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). reports on efforts by industry to provide support for use of RoboTest technology in their safety platform. Another current effort is providing support for implementation of RoboTest results in a prized testing tool adopted by major players in the cyber-physical industry. An incoming Royal Academy of Engineering Fellowship is pursuing technology transfer by extending the result to deal with humans in the loop. Colleagues in academia are also building on our work to develop their own research independently. An example is reported in 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). Finally, we are engaging with potential users through presentations at Sheffield Robotics event. |
| First Year Of Impact | 2018 |
| Sector | Digital/Communication/Information Technologies (including Software),Transport |
| Impact Types | Cultural,Societal,Economic |
| Description | 1000 Talents Programme |
| Amount | ¥1,950,000 (CNY) |
| Organisation | National Science Foundation China |
| Sector | Public |
| Country | China |
| Start | 11/2019 |
| End | 11/2024 |
| Description | Aarhus University Centre for Digital Twins |
| Amount | 970,392 kr. (DKK) |
| Funding ID | 2018-019 |
| Organisation | Aarhus University |
| Sector | Academic/University |
| Country | Denmark |
| Start | 11/2019 |
| End | 11/2024 |
| Description | Chair in Emerging Technologies |
| Amount | £1,300,000 (GBP) |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 03/2018 |
| End | 02/2028 |
| Description | Chair in Emerging Technologies Top-Up Award 1 |
| Amount | £55,000 (GBP) |
| Funding ID | CiET1819\TUA\11 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 03/2019 |
| End | 02/2020 |
| Description | Chair in Emerging Technologies Top-Up Award 2 |
| Amount | £55,000 (GBP) |
| Funding ID | CiET1920\TUA\13 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 03/2020 |
| End | 02/2021 |
| Description | Chair in Emerging Technologies Top-Up Award 4 |
| Amount | £55,000 (GBP) |
| Funding ID | CiET1920\TUA\2021\4 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 03/2021 |
| End | 02/2022 |
| Description | CyPhyAssure: Compositional Safety Assurance for Cyber-Physical Systems |
| Amount | £562,549 (GBP) |
| Funding ID | EP/S001190/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 06/2018 |
| End | 07/2021 |
| Description | EMRP |
| Amount | € 100,000 (EUR) |
| Funding ID | NEW06-REG4(UoY) |
| Organisation | European Association of National Metrology Institutes (EURAMET) |
| Sector | Charity/Non Profit |
| Country | Germany |
| Start | 06/2014 |
| End | 05/2015 |
| Description | EPSRC responsive mode |
| Amount | £1,029,474 (GBP) |
| Funding ID | EP/H017461/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 06/2010 |
| End | 09/2015 |
| Description | Horizon 2020 |
| Amount | € 7,000,000 (EUR) |
| Organisation | European Commission |
| Sector | Public |
| Country | European Union (EU) |
| Start | 01/2015 |
| End | 12/2017 |
| Description | Mini Centre for Doctoral Training. Albert: Autonomous Robotic Systems for Laboratory Experiments |
| Amount | £1,000,000 (GBP) |
| Organisation | University of York |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 04/2023 |
| End | 12/2027 |
| Description | RAEng Brazil 1 |
| Amount | £24,000 (GBP) |
| Funding ID | NRCP1617/5/68 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 06/2016 |
| End | 07/2017 |
| Description | RAEng Brazil 2 |
| Amount | £24,000 (GBP) |
| Funding ID | NRCP1617/6/164 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 01/2017 |
| End | 01/2018 |
| Description | Regional Engagement Awards |
| Amount | £75,000 (GBP) |
| Funding ID | REA1920\3\20 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 01/2020 |
| End | 12/2023 |
| Description | Seventh Framework Programme |
| Amount | € 6,000,000 (EUR) |
| Funding ID | 287829 |
| Organisation | European Commission |
| Sector | Public |
| Country | European Union (EU) |
| Start | 10/2011 |
| End | 09/2014 |
| Description | UKRI Trustworthy Autonomous Systems Node in Resilience |
| Amount | £3,033,177 (GBP) |
| Funding ID | EP/V026747/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 11/2020 |
| End | 04/2024 |
| Description | UKRI Trustworthy Autonomous Systems Node in Verifiability |
| Amount | £2,923,652 (GBP) |
| Funding ID | EP/V026801/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 11/2020 |
| End | 04/2024 |
| Description | Aarhus University Centre for Digital Twins |
| Organisation | Aarhus University |
| Department | School of Engineering |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Research collaboration with Professor Peter Gorm Larsen at Aarhus University's Centre for Digital Twins. Appointment as Adjunct Professor with support for activities, including regular visits. Appointment of Larsen as Visiting Professor at York. |
| Collaborator Contribution | Collaboration on research papers and research proposals. Joint supervision of students at Aarhus. |
| Impact | Collaboration with Cláudio Gomes on a paper: Uncertainty quantification and runtime monitoring using environment-aware digital twins. Paper accepted for ISoLA conference 2020, but delayed to 2021 because of pandemic. |
| Start Year | 2019 |
| Description | Adjunct Professorship, Southwest University, Chongqing, China |
| Organisation | Southwest University |
| Country | China |
| Sector | Academic/University |
| PI Contribution | Collaboration on a joint research project on human-cyber-physical systems. Appointment as Adjunct professor at Southwest University. Supervision of joint research students at Southwest University. Personal research fund for JCPW at Southwest University. Collaboration on the verification of neural networks. |
| Collaborator Contribution | Joint research papers and research proposals. Proposed joint research laboratory. Joint direction of FM4AI research programme. |
| Impact | Published a paper: Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, Jim Woodcock: Learning Safe Neural Network Controllers with Barrier Certificates. SETTA 2020: 177-185 |
| Start Year | 2019 |
| Description | Applicable Formal Methods |
| Organisation | Aarhus University |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Expertise in theory and practice of formal methods. |
| Collaborator Contribution | Expertise in theory and practice of formal methods. |
| Impact | Publications: 1. Mario Gleirscher, Simon Foster, Jim Woodcock: New Opportunities for Integrated Formal Methods. ACM Comput. Surv. 52(6): 117:1-117:36 (2020) 2. Mario Gleirscher, Jaco van de Pol, Jim Woodcock: A Manifesto for Applicable Formal Methods. CoRR abs/2112.12758 (2021) 3. Mario Gleirscher, Jaco van de Pol, Jim Woodcock: Proceedings First Workshop on Applicable Formal Methods, AppFM@FM 2021, virtual, 23rd November 2021. EPTCS 349, 2021 Workshop: First Workshop on Applicable Formal Methods, AppFM@FM 2021 |
| Start Year | 2020 |
| Description | Applicable Formal Methods |
| Organisation | University of Bremen |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | Expertise in theory and practice of formal methods. |
| Collaborator Contribution | Expertise in theory and practice of formal methods. |
| Impact | Publications: 1. Mario Gleirscher, Simon Foster, Jim Woodcock: New Opportunities for Integrated Formal Methods. ACM Comput. Surv. 52(6): 117:1-117:36 (2020) 2. Mario Gleirscher, Jaco van de Pol, Jim Woodcock: A Manifesto for Applicable Formal Methods. CoRR abs/2112.12758 (2021) 3. Mario Gleirscher, Jaco van de Pol, Jim Woodcock: Proceedings First Workshop on Applicable Formal Methods, AppFM@FM 2021, virtual, 23rd November 2021. EPTCS 349, 2021 Workshop: First Workshop on Applicable Formal Methods, AppFM@FM 2021 |
| Start Year | 2020 |
| Description | Butterfield TCD UTP |
| Organisation | Trinity College Dublin |
| Department | School of Computer Science and Statistics |
| Country | Ireland |
| Sector | Academic/University |
| PI Contribution | I have been collaborating with Andrew Butterfield since 2002 on Unifying Theories of Programming (UTP) and the formal semantics of of real-time, hybrid, and probabilistic systems. We meet regularly (at least twice a year) and have published 10 joint papers (five journal and five refereed conference papers). I have made contributions in foundations of UTP (including donating extensive course materials) and in applications to systems of systems and robotic and autonomous systems. |
| Collaborator Contribution | Andrew Butterfield at TCD has made contributions to understanding hardware/software co-design and real-time and probabilistic systems. He contributed a strong background in functional programming. |
| Impact | Outputs: DOIs: 10.1007/978-3-319-47166-2_26 10.1016/j.scico.2008.09.014 10.1109/TASE.2009.57 10.1109/ICECCS.2008.35 10.1109/ICECCS.2007.23 10.1007/978-3-540-73210-5_5 10.1016/j.entcs.2006.04.026 10.1007/s10009-004-0181-6 10.1016/S1571-0661(04)80821-1 10.1016/S1571-0661(04)80762-X The collaboration is multi-disciplinary, involving computer science and electronic engineering. |
| Description | CSP-based testing |
| Organisation | University of Bremen |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | Expertise in CSP and its semantics |
| Collaborator Contribution | Expertise on testing and automation |
| Impact | J. Peleska, W. l. Huang, and A. L. C. Cavalcanti. Finite complete suites for CSP refinement testing. Science of Computer Programming, 179:1 -- 23, 2019. A. L. C. Cavalcanti, W.-L. Huang, J. Peleska, and J. C. P. Woodcock. CSP and Kripke Structures. In M. Leucker, C. Rueda, and F. D. Valencia, editors, Theoretical Aspects of Computing, pages 505--523. Springer, 2015. |
| Start Year | 2015 |
| Description | Circus foundations and Isabelle/UTP |
| Organisation | Galois, Inc. |
| Country | United States |
| Sector | Private |
| PI Contribution | This is a collaboration that has just started. We are going to provide expertise on the techniques. |
| Collaborator Contribution | They are taking a lead to mechanise the techniques and apply them on Rigorous Digital Engineering. |
| Impact | Development of theories and techniques, and their application to industrial case studies. |
| Start Year | 2022 |
| Description | Collaboration on RoboSim language: semantics, verification, examples, tools. |
| Organisation | Federal University of Pernambuco |
| Country | Brazil |
| Sector | Academic/University |
| PI Contribution | Training on robotics |
| Collaborator Contribution | Partnership in the design and implementation of RoboSim |
| Impact | Joint papers. |
| Start Year | 2017 |
| Description | Collaboration on RoboWorld language: syntax, semantics, examples, tools |
| Organisation | UFPE |
| Country | Brazil |
| Sector | Academic/University |
| PI Contribution | Expertise on robotics, the RoboChart language, and CyPhyCircus semantics |
| Collaborator Contribution | Expertise on controlled natural languages, partnership in the design and implementation of RoboWorld |
| Impact | Development of the RoboWorld language and a prototype tool for it, journal paper under review |
| Start Year | 2019 |
| Description | Collaboration on Social, Legal, Ethical, Empathetic and Cultural (SLEEC) aspects of autonomous agents with the TAS Resilience Node |
| Organisation | University of York |
| Department | Department of Computer Science |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Expertise on the formal semantics of RoboChart and definition of conformance relation for checking satisfaction of design models against SLEEC rules. |
| Collaborator Contribution | Expertise on Social, Legal, Ethical, Empathetic and Cultural (SLEEC) aspects for Autonomous Agents. |
| Impact | Joint work under way and contributing to the writing of joint journal paper. |
| Start Year | 2022 |
| Description | Collaboration with Univesity of Agder, NMBU, and ABB Robotics |
| Organisation | ABB Group |
| Country | Switzerland |
| Sector | Private |
| PI Contribution | We have provided insight into the use of tools and techniques for modelling and verification of a High-Voltage Controller (HVC) robotic system. |
| Collaborator Contribution | They have brought a case study of a High-Voltage Controller, which is at the core of a painting robot developed at ABB Robotics. They have used RoboChart and RoboTool to model the software controller and perform formal verification of safety properties. Work is ongoing towards verification including a model of the physical robotic platform. |
| Impact | * A case study, including two models. * Improvements to the implementation of the semantics of RoboChart for model-checking. * A publication: Murray Y, Anisi D, Sirevåg M, Ribeiro P, Hagag R. (2020). Safety Assurance of a High Voltage Controller for an Industrial Robotic System. Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings. (pp. 45-63). |
| Start Year | 2020 |
| Description | Collaboration with Univesity of Agder, NMBU, and ABB Robotics |
| Organisation | Norwegian University of Life Sciences (NMBU) |
| Country | Norway |
| Sector | Academic/University |
| PI Contribution | We have provided insight into the use of tools and techniques for modelling and verification of a High-Voltage Controller (HVC) robotic system. |
| Collaborator Contribution | They have brought a case study of a High-Voltage Controller, which is at the core of a painting robot developed at ABB Robotics. They have used RoboChart and RoboTool to model the software controller and perform formal verification of safety properties. Work is ongoing towards verification including a model of the physical robotic platform. |
| Impact | * A case study, including two models. * Improvements to the implementation of the semantics of RoboChart for model-checking. * A publication: Murray Y, Anisi D, Sirevåg M, Ribeiro P, Hagag R. (2020). Safety Assurance of a High Voltage Controller for an Industrial Robotic System. Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings. (pp. 45-63). |
| Start Year | 2020 |
| Description | Collaboration with Univesity of Agder, NMBU, and ABB Robotics |
| Organisation | University of Agder |
| Country | Norway |
| Sector | Academic/University |
| PI Contribution | We have provided insight into the use of tools and techniques for modelling and verification of a High-Voltage Controller (HVC) robotic system. |
| Collaborator Contribution | They have brought a case study of a High-Voltage Controller, which is at the core of a painting robot developed at ABB Robotics. They have used RoboChart and RoboTool to model the software controller and perform formal verification of safety properties. Work is ongoing towards verification including a model of the physical robotic platform. |
| Impact | * A case study, including two models. * Improvements to the implementation of the semantics of RoboChart for model-checking. * A publication: Murray Y, Anisi D, Sirevåg M, Ribeiro P, Hagag R. (2020). Safety Assurance of a High Voltage Controller for an Industrial Robotic System. Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings. (pp. 45-63). |
| Start Year | 2020 |
| Description | D'Souza IISc Verification |
| Organisation | Indian Institute of Science Bangalore |
| Department | Department of Computer Science and Automation |
| Country | India |
| Sector | Academic/University |
| PI Contribution | My team contributed expertise in formal specification, refinement, and verification of software. We contributed to the verification of FreeRTOS, the popular open-source real-time operating system. We helped our Indian colleagues develop expertise in Z and Z/Eves and helped them apply it to verification problems. |
| Collaborator Contribution | Colleagues at the Indian Institute of Science and General Motors India helped us to understand the FreeRTOS code and extract suitable abstract specifications of aspects of its behaviour. |
| Impact | Three projects funded by the British Council, the Royal Academy of Engineering, and the Robert Bosch Centre for Cyber-Physical Systems (total value £175k). One conference paper (10.1007/978-3-319-25423-4_11). One journal paper (10.1007/s00165-014-0308-9). Two Phd theses: Sumesh Divakaran: A Refinement-Based Methodology for Verifying Abstract Data Type Implementations (IISc, 2015). Shu Cheng: Formally modelling and verifying the FreeRTOS real-time operating system (York, 2014). |
| Start Year | 2010 |
| Description | Distinguished Visiting Professor |
| Organisation | Fudan University |
| Country | China |
| Sector | Academic/University |
| PI Contribution | New appointment for Prof Timmis to explore further applications of the technology in intelligent robotics. |
| Collaborator Contribution | Initial discussions on case studies and possible research student supervision. |
| Impact | None as yes. |
| Start Year | 2021 |
| Description | ECNU - Shanghai UPPAL |
| Organisation | East China Normal University (ECNU) |
| Country | China |
| Sector | Academic/University |
| PI Contribution | We bring in expertise in robotics, simulation, and model-based engineering, including the design and semantics of RoboSim. |
| Collaborator Contribution | They bring in expertise in timed and probabilistic model checking, and verification using bisimulation. |
| Impact | A tool under development and a paper in preparation. |
| Start Year | 2020 |
| Description | FMI Step Negotiation |
| Organisation | Aarhus University |
| Department | Department of Engineering |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Meetings to discuss how to verify co-simulation algorithms with algebraic loops and adaptive steps. Our insight is to use angelic nondeterminism to specify backtracking. This requires new theories of state-rich, reactive, angelic nondeterminism. |
| Collaborator Contribution | Aarhus are the problem owners. They contributed expertise in the functional mock-up interface (FMI) and the problems of adaptive co-simulaiton. |
| Impact | Paper: Simon Thrane Hansen, Cláudio Gomes, Maurizio Palmieri, Casper Thule, Jaco van de Pol, Jim Woodcock: Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps. FMICS 2021: 3-20 DOI: 10.1007/978-3-030-85248-1_1 |
| Start Year | 2021 |
| Description | FitzLarsen CPS EU |
| Organisation | Aarhus University |
| Department | School of Engineering |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Our collaboration has involved two major EU projects. My research team brought expertise in modelling, formal semantics, mechanised proof, and model checking. |
| Collaborator Contribution | Newcastle made contribution in modelling and methods. Aarhus made contributions in tool building. |
| Impact | Also see http://www.compass-research.eu/. Outputs: Funding for two large EU projects. Publications: 8 conference papers, 4 journal papers, 2 book chapters. Citations: > 600 in total. Multi-disciplinary collaboration covering systems, software, hardware, control theory, and electronics. |
| Start Year | 2009 |
| Description | Formal methods in security |
| Organisation | Aarhus University |
| Department | Department of Engineering |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Expertise in formal methods in security |
| Collaborator Contribution | Expertise in formal methods in security |
| Impact | Technical report: Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter Würtz Vinther Tran-Jørgensen, Jim Woodcock: A Survey of Practical Formal Methods for Security. CoRR abs/2109.01362 (2021) Accepted for publication in ACM Formal Aspects of Computing. |
| Start Year | 2020 |
| Description | Formal methods in security |
| Organisation | University of Surrey |
| Department | Department of Computing |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Expertise in formal methods in security |
| Collaborator Contribution | Expertise in formal methods in security |
| Impact | Technical report: Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter Würtz Vinther Tran-Jørgensen, Jim Woodcock: A Survey of Practical Formal Methods for Security. CoRR abs/2109.01362 (2021) Accepted for publication in ACM Formal Aspects of Computing. |
| Start Year | 2020 |
| Description | Hybrid Model Checking - CORA |
| Organisation | Technical University of Munich |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | We bring expertise in robotics, the design and semantics of the RoboWorld language, and the CyPhyCircus hybrid process algebra. |
| Collaborator Contribution | They bring expertise in hybrid model checking, and development on the CORA hybrid model checker to support our models. |
| Impact | Models in CORA based on the semantics of RoboWorld, testing and enhancement of the CORA hybrid model checker. |
| Start Year | 2022 |
| Description | Interaction trees |
| Organisation | Seoul National University |
| Country | Korea, Republic of |
| Sector | Academic/University |
| PI Contribution | Expertise in UTP semantics and Isabelle. |
| Collaborator Contribution | Expertise in interaction trees. |
| Impact | Technical report: Simon Foster, Chung-Kil Hur, Jim Woodcock: Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. CoRR abs/2105.05133 (2021) Implementation in Isabelle/UTP. Contributions to undergraduate and postgraduate teaching: PROF module. |
| Start Year | 2021 |
| Description | Lectures on Probabilistic Robotics |
| Organisation | Aarhus University |
| Department | Department of Engineering |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Outreach and dissemination through research-based teaching. |
| Collaborator Contribution | Providing an audience of engineering students. |
| Impact | Lecture not4s, slides, and videos. |
| Start Year | 2022 |
| Description | Lectures on Programming and Modelling |
| Organisation | Aarhus University |
| Department | Department of Engineering |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Research-based teaching. |
| Collaborator Contribution | Provision of engineering student audience. |
| Impact | Lecture notes, slides, and videos. |
| Start Year | 2022 |
| Description | Reducing the Cyber Attack Surface |
| Organisation | Aarhus University |
| Department | Department of Engineering |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Survey of verifiable computation techniques. Experiments. Proposal for future work. |
| Collaborator Contribution | Contributions to report. |
| Impact | Reports. Draft publications. |
| Start Year | 2022 |
| Description | Reducing the Cyber Attack Surface |
| Organisation | D-RisQ |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Survey of verifiable computation techniques. Experiments. Proposal for future work. |
| Collaborator Contribution | Contributions to report. |
| Impact | Reports. Draft publications. |
| Start Year | 2022 |
| Description | Reducing the Cyber Attack Surface |
| Organisation | Defence Science & Technology Laboratory (DSTL) |
| Country | United Kingdom |
| Sector | Public |
| PI Contribution | Survey of verifiable computation techniques. Experiments. Proposal for future work. |
| Collaborator Contribution | Contributions to report. |
| Impact | Reports. Draft publications. |
| Start Year | 2022 |
| Description | Royal Academy of Engineering Industry Fellowship |
| Organisation | Thales Group |
| Department | Thales UK Limited |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Co-supervision of student and industry fellows. |
| Collaborator Contribution | We are developing a technique to model and verify mobile and autonomous robots with humans in the loop. |
| Impact | Multi-disciplinary: Engineering and Psychology. |
| Start Year | 2021 |
| Description | Simomics Robotics |
| Organisation | Simomics Ltd |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Expertise on modelling and verification of robotics systems. |
| Collaborator Contribution | Tools for modelling auditing and assurance cases. |
| Impact | A tool is under development. |
| Start Year | 2020 |
| Description | Sound simulation of robotic applications |
| Organisation | Federal University of Pernambuco |
| Country | Brazil |
| Sector | Academic/University |
| PI Contribution | We have brought to them expertise on the results and approaches to modelling and verifying robotic applications, and developing simulations. |
| Collaborator Contribution | They have brought in experience in model-based software engineering, compositional verification, testing, and probabilistic model checking. They have employed a research assistant to to work on the project and collaborate with our group. Together, we are developing a domain-specific language for modelling simulations. The language has a formal semantics under development. They are in charge of developing tool support for this language, and developing tool support for probabilistic reasoning. |
| Impact | Tools are under development and papers are submitted. |
| Start Year | 2017 |
| Description | Transport Systems Catapult - Autonomous Vehicle |
| Organisation | Transport Systems Catapult |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Modelling, analysis and simulation of the control system of an autonomous vehicle. Using the tools and techniques developed in RoboCalc, we will explore the limits of what is possible to model, analyse and simulate with respect to a complex realistic controller where safety concerns are of utmost importance. |
| Collaborator Contribution | They are experts in the development of transport systems. As well as their expertise, they will provides us with documentation and source code regarding the specific case study. |
| Impact | *A case study, the largest RoboChart model to date. *Preliminary analysis results based on model checking technology. *The model and results will be published in a book, which is currently at the final stages of publication. |
| Start Year | 2017 |
| Description | Uncertainty |
| Organisation | King's College London |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Discussions between the University of York and King's College London on a future research proposal. |
| Collaborator Contribution | Discussions between the University of York and King's College London on a future research proposal. |
| Impact | Draft research proposal. |
| Start Year | 2022 |
| Description | Uncertainty in autonomous systems |
| Organisation | King's College London |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Definition of probabilistic semantics in UTP and implementation in Isabelle/UTP. |
| Collaborator Contribution | Problems, examples, case studies. |
| Impact | No outputs yet. |
| Start Year | 2021 |
| Description | Uncertainty in autonomous systems |
| Organisation | University of York |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Definition of probabilistic semantics in UTP and implementation in Isabelle/UTP. |
| Collaborator Contribution | Problems, examples, case studies. |
| Impact | No outputs yet. |
| Start Year | 2021 |
| Description | VSR collaborations |
| Organisation | Microsoft Research |
| Department | Microsoft Research Cambridge |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Organising the UK's contribution to the Verified Software Initiative. |
| Collaborator Contribution | Suppliers of case studies, verification technology, challenge project prizes, organisers of workshops. |
| Impact | Collection of verification case studies for experimentation by the verification community. |
| Start Year | 2006 |
| Description | VSR collaborations |
| Organisation | Praxis Systems Ltd |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Organising the UK's contribution to the Verified Software Initiative. |
| Collaborator Contribution | Suppliers of case studies, verification technology, challenge project prizes, organisers of workshops. |
| Impact | Collection of verification case studies for experimentation by the verification community. |
| Start Year | 2006 |
| Description | Verification and uncertainties in self-integrating systems |
| Organisation | Aarhus University |
| Department | Department of Engineering |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Expertise in unification of semantics and verification techniques. |
| Collaborator Contribution | Expertise in self-integrating systems and uncertainty. |
| Impact | Publication: Lukas Esterle, Barry Porter, Jim Woodcock: Verification and Uncertainties in Self-integrating System. ACSOS-C 2021: 220-225 DOI: 10.1109/ACSOS-C52956.2021.00050 |
| Start Year | 2021 |
| Description | Verification and uncertainties in self-integrating systems |
| Organisation | Lancaster University |
| Department | School of Computing and Communications |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Expertise in unification of semantics and verification techniques. |
| Collaborator Contribution | Expertise in self-integrating systems and uncertainty. |
| Impact | Publication: Lukas Esterle, Barry Porter, Jim Woodcock: Verification and Uncertainties in Self-integrating System. ACSOS-C 2021: 220-225 DOI: 10.1109/ACSOS-C52956.2021.00050 |
| Start Year | 2021 |
| Description | Verification grand challenge history |
| Organisation | Altran |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | History of the Verified Software Initiative |
| Collaborator Contribution | Personal accounts of contributions to the Verified Software Initiative. |
| Impact | Publication: Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, Thomas Santen: Verification in the Grand Challenge. Theories of Programming 2021: 125-156 DOI: 10.1145/3477355.3477363 |
| Start Year | 2021 |
| Description | Verification grand challenge history |
| Organisation | Technical University Berlin |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | History of the Verified Software Initiative |
| Collaborator Contribution | Personal accounts of contributions to the Verified Software Initiative. |
| Impact | Publication: Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, Thomas Santen: Verification in the Grand Challenge. Theories of Programming 2021: 125-156 DOI: 10.1145/3477355.3477363 |
| Start Year | 2021 |
| Description | bangalore-2018 |
| Organisation | Indian Institute of Science Bangalore |
| Country | India |
| Sector | Academic/University |
| PI Contribution | Newton grant from RAEng held by IIIT-B. Contributions on refinement of simulink models. |
| Collaborator Contribution | Research in refinement of simulink models. |
| Impact | Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. RAMiCS 2018: 205-224 Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. CoRR abs/1806.02101 (2018) |
| Start Year | 2018 |
| Description | butterfield-tcd-march-2018 |
| Organisation | Trinity College Dublin |
| Department | Trinity Biomedical Sciences Institute |
| Country | Ireland |
| Sector | Hospitals |
| PI Contribution | Research discussions at TCD. |
| Collaborator Contribution | Research discussions. |
| Impact | Discussions on future research collaborations. |
| Start Year | 2018 |
| Description | chongqing-2-2018 |
| Organisation | Southwest University |
| Country | China |
| Sector | Academic/University |
| PI Contribution | Royal Society China Cost Share Programme |
| Collaborator Contribution | Research contributions. |
| Impact | None yet. |
| Start Year | 2018 |
| Description | chongqing2018 |
| Organisation | Southwest University |
| Country | China |
| Sector | Academic/University |
| PI Contribution | Royal Society China Cost Share Programme. |
| Collaborator Contribution | Rsearch contributions. |
| Impact | No outputs yet. |
| Start Year | 2018 |
| Description | digit-2018 |
| Organisation | Aarhus University |
| Department | Aarhus Institute of Advanced Studies |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Planning for future collaboration. |
| Collaborator Contribution | Research exchanges. |
| Impact | Proposal to Grundfos Foundation. |
| Start Year | 2018 |
| Description | peleska-testing-2018 |
| Organisation | University of Bremen |
| Country | Germany |
| Sector | Academic/University |
| PI Contribution | Rsearch discussions. |
| Collaborator Contribution | Rsearch discussions. |
| Impact | Research proposals. |
| Start Year | 2018 |
| Description | 18th International Summer School on Trustworthy Software |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | Ana Cavalcanti and Jim Woodcock led courses on Software Engineering for Robotics and Isabelle/HOL as part of the 18th International Summer School on Trustworthy Software organised by the School of Software Engineering of East China Normal University. RoboStar colleagues James Baxter , Gustavo Carvalho , Alvaro Miyazawa , Pedro Ribeiro and Matt Windsor delivered practicals and seminars. |
| Year(s) Of Engagement Activity | 2022 |
| Description | 18th International Summer School on Trustworthy Software |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | In August 2022, we delivered a series of lectures via video link to graduate students at East China Normal University (ECNU) in Shanghai, China as part of the 18th International Summer School on Trustworthy Software organised by the Software Engineering Institute at the ECNU. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://seisummerschool.github.io/2022/ |
| Description | Aarhus Lectures on probabilistic robotics |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Undergraduate students |
| Results and Impact | I delivered a series of six lectures on probabilistic robotic control to undergraduates in engineering at Aarhus University. The lectures were prepared as curated videos with lecture notes. |
| Year(s) Of Engagement Activity | 2021 |
| Description | Are you Talking to your Autonomous Car? (Maybe you should!) |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Public/other audiences |
| Results and Impact | Ana Cavalcanti featured as a speaker in the latest Living with AI Podcast of the TAS Hub. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://www.buzzsprout.com/1447474/11041372 |
| Description | Bristol BAME STEM seminar on Software Engineering for Robotics |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | Webinar on my career journey and research interests to a wide range of scientists and Science Administrators for wider dissemination. |
| Year(s) Of Engagement Activity | 2023 |
| Description | CUP journal. Research Directions: Cyber-Physical Systems |
| Form Of Engagement Activity | A magazine, newsletter or online publication |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Development and launch of a new journal. |
| Year(s) Of Engagement Activity | 2022,2023 |
| URL | https://www.cambridge.org/core/journals/research-directions-cyber-physical-systems |
| Description | China Lectures on probabilistic robotics |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Undergraduate students |
| Results and Impact | I delivered a series of six lectures on probabilistic robotic control. |
| Year(s) Of Engagement Activity | 2021 |
| Description | Course at School of Software, Northwest Polytechnical University, Xi'an, China |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | I contributed to a tutorial on the use of the RoboChart notation for formal verification of robotic applications. |
| Year(s) Of Engagement Activity | 2021 |
| Description | CyPhyAssure Spring School |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Participation in Spring School on the assurance of cyber-physical systems. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://www.cs.york.ac.uk/circus/CyPhyAssure/school/ |
| Description | DIGIT Advisory Board |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Participation in the advisory board of the center for digital twins at Aarhus University, |
| Year(s) Of Engagement Activity | 2018 |
| Description | Dagstuhl seminar on Integrated Rigorous Analysis in Cyber-Physical Systems Engineering |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Week-long seminar of world experts on cyber-physical systems. Seminar report. Publication. |
| Year(s) Of Engagement Activity | 2023 |
| URL | https://www.dagstuhl.de/en/seminars/seminar-calendar/seminar-details/23041 |
| Description | ECNU summer school |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | In August 2022, we delivered a series of lectures via video link to graduate students at East China Normal University (ECNU) in Shanghai, China as part of a summer school on Trustworthy Systems. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://seisummerschool.github.io/2022/ |
| Description | FM 2019 |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Talks and discussions with international colleagues. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Formally Verified Animation for RoboChart using Interaction Trees at ICFEM2022 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | A talk about "Formally Verified Animation for RoboChart using Interaction Trees" given at the conference ICFEM2022 |
| Year(s) Of Engagement Activity | 2022 |
| URL | http://maude.ucm.es/ICFEM22/index.html |
| Description | Guest lecture on model-based software engineering for robotics |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Undergraduate students |
| Results and Impact | I delivered a two-part guest lecture on "Model-based software engineering for robotics", as part of the undegratuate module "Model-Driven Engineering" (Computer Science, University of York), based on outputs of my research on sound model-transformation from RoboChart to RoboSim. |
| Year(s) Of Engagement Activity | 2022 |
| Description | Huawei Research Forum |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | Presentation on formal methods for assurance of security-related software in Huawei 5G products. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Huawei Research Symposium |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | Presentation of my research agenda to Huawei engineers. I gave advice on future research policy for their company. |
| Year(s) Of Engagement Activity | 2019 |
| Description | IFIP WG 2.3 Programming Methodology |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Hosted meeting of IFIP WG 2.3 on Programming Methodology. Organised scientific and social agenda, chaired the meeting, and gave an extended scientific talk. I involved my doctoral students and research assistants in the meeting. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://ifip-tc2-wg23.paluno.uni-due.de/?page_id=455 |
| Description | Invited Lecture at University of Sheffield |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Postgraduate students |
| Results and Impact | the research at a level accessible to young researchers. |
| Year(s) Of Engagement Activity | 2021 |
| Description | Invited course at the School of Software, Northwest Polytechnical University, Xi'an, China |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | This is a school organised by a consortium of Chinese universities that provides younger researchers with the background on the state of the art in the area of software engineering. The course sparked questions and discussion afterwards. |
| Year(s) Of Engagement Activity | 2021 |
| Description | Invited course at the School of the International Colloquium on Theoretical Aspects of Computing |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | This is a school associated with an international conference that provides younger researchers with the background on the state of the art in the area of theoretical aspects of computing. The course sparked questions and discussion afterwards, and led to a publication. |
| Year(s) Of Engagement Activity | 2021 |
| URL | https://ictac2021.github.io/school.html |
| Description | Invited lecture University of Leicester |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Postgraduate students |
| Results and Impact | Present the research at a level accessible to young researchers. |
| Year(s) Of Engagement Activity | 2018 |
| URL | https://www2.le.ac.uk/departments/informatics/news/researchevents/external |
| Description | Invited lecture at the International School on Formal Methods and Theoretical Informatics (ETMF) |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Undergraduate students |
| Results and Impact | This is a school associated with an international conference that provides younger students with the background to follow the paper presentations in the conference. The course sparked questions and discussion afterwards and during the main event. |
| Year(s) Of Engagement Activity | 2021 |
| URL | https://sites.google.com/computacao.ufcg.edu.br/sbmf2021/program |
| Description | Invited talk at BCS on How can we define operational requirements in robotics? |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | On the 9th of May, Ana Cavalcanti lead a seminar on "How can we define operational requirements in robotics?" together with colleagues James Baxter and Gustavo Carvalho . The event was organised by BCS London Central Branch and BCS North London branch, for IT professionals. |
| Year(s) Of Engagement Activity | 2022 |
| Description | Invited talk at HIS (High- Integrity Software) 2019 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Industry/Business |
| Results and Impact | Now in its sixth year, the mission of the High Integrity Software conference is to share challenges, best practice and experience between software engineering practitioners. The conference features talks from industrial and academic specialists which disseminate experience and knowledge of important techniques and methods that are applicable across industry sectors. I have presented the technology developed in our researcher. It sparked questions and discussion, afterwards, and later contacts with a view to exchange ideas and collaborate. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://www.his-2017.co.uk/ |
| Description | Invited talk at the IROS2021 Workshop on Standardised Software Frameworks for Robotics in Nuclear |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | This was a workshop organised by colleagues in industry. It gave us the opportunity to present our results and spark discussion with practitioners who are themselves interested in technological developments in the area. |
| Year(s) Of Engagement Activity | 2021 |
| URL | https://ukaeaevents.com/2021-ieee-rsj/ |
| Description | Invited talk at the York & North Yorkshire LEP Skills Conference |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Professional Practitioners |
| Results and Impact | Ana Cavalcanti delivered an invited talk at the York & North Yorkshire LEP Skills Conference on "Software Engineering for Robotics in Industry 4.0". The talk can be watched on YouTube |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://www.ynylep.com/news/festival-of-engagement/event/id/2220 |
| Description | Invited talk on probabilistic robotics |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Undergraduate students |
| Results and Impact | I delivered an invited talk at a summer school in Shanghai. |
| Year(s) Of Engagement Activity | 2021 |
| Description | Newton Institue Workshop |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | I gave a talk about the impact of verification technology on practical application. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Opening of Aarhus Centre for Digital Twins |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | Keynote talk on research direction at the opening of the Centre for Digital Twins at Aarhus University. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://digit.au.dk/research-projects/centre-for-digital-twins/ |
| Description | Organisation of RoboStar and YorRobots Industry Exhibition |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | On 11-12 October YorRobots and RoboStar hosted an Industry Exhibition. There were talks and demonstrations by RoboStar colleagues and from YorRobots, The Institute for Safe Autonomy, Adelard, AgroIntelli, BAE, Bristol Robotics Lab, ClearSy, Chemspeed Technologies, Connected Places, LabMan, LDRA, DRis-Q, Dyson, RobotCenter, ShadowRobot, Thales and VSI. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://robostar.cs.york.ac.uk/events/yrie2022/ |
| Description | Organised and Participated in Computer Science Postgraduate welcome Research Showcase and Panel |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Postgraduate students |
| Results and Impact | Organised a postgraduate welcome week event to showcase existing Computer Science research within the University of York, alongside chairing a panel of existing students sharing research experiences. The research showcase was a series of short presentations. This has sparked interest from new postgraduate researchers in my own research. |
| Year(s) Of Engagement Activity | 2022 |
| Description | Presentation at IFIP WG 2.3 Meeting |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Other audiences |
| Results and Impact | Recent work on priorities, related to the formal semantics of RoboChart and RoboSim, was presented to the Working Group on Programming Methodology, as well as to the invited speakers. The goal of the presentation was to disseminate our work and receive feedback on ongoing research. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Presentation at IFIP WG 2.3 Meeting |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Other audiences |
| Results and Impact | Our work on modelling for robotics was presented to the members of the Working Group on Programming Methodology, as well as to the invited observers. The goal of the presentation was to disseminate our work and receive feedback on current research. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Presentation at Pint of Science Festival 2018 in York |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Public/other audiences |
| Results and Impact | The Pint of Science festival is run every year bringing researchers to local pubs to present their work to the general public. In this talk, we motivated our work using robotic demonstrators and presented our main results. The talk was followed by a number of interesting questions from the public. |
| Year(s) Of Engagement Activity | 2018 |
| URL | https://pintofscience.co.uk/event/are-you-sure-you-are-safe |
| Description | Presentation at Pint of Science Festival 2019 in York |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Public/other audiences |
| Results and Impact | The Pint of Science festival is run every year bringing researchers to local pubs to present their work to the general public. In this talk, we presented our work on modelling and verifying the robot software, with particular focus on application of our approach to robot swarms. The talk was followed by a number of interesting questions from the public. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://pintofscience.co.uk/event/-blurred-lines-boundaries-between-man-and-machine |
| Description | Presentation at RoboStar and YorRobots Industry Exhibition |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | On 11th October 2022, I gave a talk and presented a poster on the semantics of the RoboWorld language and the use of hybrid model checking to check the semantics. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://robostar.cs.york.ac.uk/events/yrie2022/ |
| Description | Presentation at meeting with BSI |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | I presented an overview of the RoboCalc and RoboTest projects at a meeting with British Standards Institution and the Assuring Autonomy International Programme at York, which discussed standards in AI, robotics and autonomy. |
| Year(s) Of Engagement Activity | 2018 |
| Description | Presentation of project to Thales |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Industry/Business |
| Results and Impact | Presentation of the project to consider possible collaboration. Six colleagues from Thales attended. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Presentations at RoboStar and YorRobots Industry Exhibition |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | On 11-12 October, I gave three talks on the work developed in the RoboCalc and RoboTest projects at an Industry Exhibition. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://robostar.cs.york.ac.uk/events/yrie2022/ |
| Description | Probabilistic modelling and verification using RoboChart and PRISM at MODELS2022 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Invited as a Journal-first paper by International Journal on Software and Systems Modeling (SoSyM) to present our work at MODELS 2022 on 27th October 2022 |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://conf.researchr.org/home/models-2022 |
| Description | Public talk as part of YorkTalks |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Public/other audiences |
| Results and Impact | About 300 people attended an event in the university The talks sparked questions and discussion afterwards, with the public, and with other colleagues involved in the event. The aim of the overall event is to showcase the very best of the University's research across seven research themes in order to exemplify our commitment to research excellence which forms a key component of the University Strategy and the Research Strategy. |
| Year(s) Of Engagement Activity | 2020 |
| URL | https://www.york.ac.uk/research/events/yorktalks/ |
| Description | RAMiCS 2021 conference |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | A talk about "Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving" in the conference RAMiCS 2021 on November 4, 2021. |
| Year(s) Of Engagement Activity | 2021 |
| URL | https://ramics19.lis-lab.fr/ |
| Description | REF 2021 Subpanel 11 |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Policymakers/politicians |
| Results and Impact | Computer Science subpanel member for Research Evaluation Framework 2021. |
| Year(s) Of Engagement Activity | 2021,2022 |
| Description | RoboSoft: software engineering for robotics |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Professional Practitioners |
| Results and Impact | RoboSoft was a two-day event that will brought together researchers working on software engineering for robotics, developers working on the next generation of robotic systems in various areas of application, and regulation authorities interested in safety of robotic systems. RoboSoft provides a platform to establish software engineering for robotics as an important discipline in computer science and electronic engineering. The objective was to establish a common understanding of the challenges that need to be addressed to ensure that results are relevant to industrial practice and regulation. The group organised the whole event and gave three presentations. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://www.raeng.org.uk/events/events-programme/2019/november/robosoft-software-engineering-for-rob... |
| Description | RoboStar and YorRobots Industry Exhibition |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | On 11th October 2022, I was a speaker in two talks on "RoboSim: software models for sound simulation" and "Trustworthy Autonomous Systems Node on Verifiability", and co-presented (as well as co-authored) three posters during the exhibition: (1) "RoboSim: software models for sound simulation"; (2) "Autonomous Fire-Fighting UAV" ; (3) "Safety Assurance of an Industrial Robotic Control System Using Hardware/Software Co-Verification" related to my on-going collaboration with the University of Agder (Norwary), Norwegian University of Life Sciences and ABB Robotics. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://robostar.cs.york.ac.uk/events/yrie2022/ |
| Description | Royal Academy of Engineering Research Forum |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Other audiences |
| Results and Impact | The Research Forum is a highlight of the Academy's activities. It showcases the world-class engineering research funded through the Academy's wide range of programmes. The event consists of a mix of keynote talks from current awardees and alumni. Awardees from across the portfolio of Academy's research schemes will also exhibit posters and demos throughout the day. The project was presented in a keynote talk. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://www.raeng.org.uk/events/events-programme/2019/november/research-forum |
| Description | Summer School |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | Second Summer School in 2023 at ECNU. |
| Year(s) Of Engagement Activity | 2023 |
| Description | Summer School lecturess |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | Lectures delivered at a Summer School at ECNU in Shanghai. |
| Year(s) Of Engagement Activity | 2022 |
| Description | Symposium for Marie-Claude Gaudel |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | I gave a talk on software engineering for robotic control. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Talk at Huawei engineering conference |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | A talk was given at Huawei's engineering conference on advance software engineering practice. |
| Year(s) Of Engagement Activity | 2022 |
| Description | Talk at Verification Future Meeting |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Industry/Business |
| Results and Impact | I gave an invited talk at this industry meeting. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://www.testandverification.com/conferences/verification-futures/vf2019 |
| Description | Tutorial at 25th Brazilian Symposium on Formal Methods |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | On 8 December 2022, Alvaro Miyazawa lead a tutorial on "RoboStar and RoboTool: Software Engineering for Robotics using Formal Methods". The tutorial was part of the 25th Brazilian Symposium on Formal Methods. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://sites.google.com/dcomp.ufs.br/sbmf2022/keynotes-tutorials?authuser=0 |
| Description | UK-RAS Network RoboTalk Podcast |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Public/other audiences |
| Results and Impact | Podcast organised by the UK-RAS network to describe research and projects of my group. |
| Year(s) Of Engagement Activity | 2022 |
| URL | https://www.ukras.org.uk/news/robot-talk-episode-thirty-out-now |
| Description | Verifiability Talk |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Study participants or study members |
| Results and Impact | Presentation of the RoboStar approach to Software Engineering for Robotics, including modelling and testing |
| Year(s) Of Engagement Activity | 2021 |
| Description | Verifiability Talk |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Study participants or study members |
| Results and Impact | Presentation on A Unifying Framework for Verifiability as part of the seminar series for the EPSRC Trusted Autonomous Systems Verifiability Node. |
| Year(s) Of Engagement Activity | 2021 |
| URL | https://www.youtube.com/watch?v=iUv5i9NYgNU |
| Description | Video on cyber-physical systems |
| Form Of Engagement Activity | A broadcast e.g. TV/radio/film/podcast (other than news/press) |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Video promoting research in cyber-physical systems. |
| Year(s) Of Engagement Activity | 2023 |
| URL | https://www.cambridge.org/core/journals/research-directions-cyber-physical-systems |
| Description | Visit by Jan Pekeska |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Other audiences |
| Results and Impact | Discussions on research collaboration. |
| Year(s) Of Engagement Activity | 2018 |
| Description | Visit by Ziming Liiu |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Visit to discuss long-term research collaboration. |
| Year(s) Of Engagement Activity | 2018 |
| Description | Visit from Southwest University |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Visit from a delegation from Southwest University, Chongqing, China. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Visit from TCD Ireland |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Other audiences |
| Results and Impact | Visit from colleagues from Trinity College Dublin. Contributions on probabilistic semantic for robotics. |
| Year(s) Of Engagement Activity | 2018,2019 |
| Description | Visit ti Aarhus University |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Visit to exchange research ideas. |
| Year(s) Of Engagement Activity | 2018 |
| Description | Visit to Chongqing |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | Workshop on formal methods for human-cyber-=physical systems. I gave talks on software engineering for robotics. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Visit to Chongqing |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Visit Southwest University to give lectures and direct doctoral students. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Visit to IISc |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Presentation of research work. Exchange of research ideas for future research proposals. |
| Year(s) Of Engagement Activity | 2018 |
| Description | Visit to IISc Bangalore |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Workshop at IISc funded by Royal Academy of Engineering. Discussed work on formal verification of operating system real-time kernels. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Visit to Malardalen University |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | External examining of a doctoral student. Interaction with academic colleagues on research directions. Interaction with industry colleagues on research directions. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Visit to Southwest University |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Study participants or study members |
| Results and Impact | Visit to exchange ideas. |
| Year(s) Of Engagement Activity | 2018 |
| Description | White Rose Retreat on Robotics |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Study participants or study members |
| Results and Impact | Discussed future collaborative in robotics. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Workshop for Advisory Board and additional representatives from academia and industry |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Industry/Business |
| Results and Impact | Meeting of the Advisory Board to report on our results from RoboCalc and kick-off RoboTest. The joint meeting of the projects was very positive. There was a lot of discussion and good feedback. Further colleagues from industry asked to join the Advisory Board afterwards. |
| Year(s) Of Engagement Activity | 2018 |
| Description | YorRobots Exhibition |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | More than 100 researchers and industrialists working in the area of robotics attended a one-day exhibition involving talks, posters, and demonstrations of work carried out in the University of York and in industry around the UK. There was plenty of opportunity for discussion and engagement. I have presented the results and the vision for RoboCalc and RoboTest, and beyond. |
| Year(s) Of Engagement Activity | 2020 |
| URL | https://www.york.ac.uk/yorrobots/news-events/yorrobots-events/2020/exhibition-2020/ |
| Description | YorRobots Industry Exhibition |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Two talks and two posters. |
| Year(s) Of Engagement Activity | 2022 |
| Description | YorRobots launch event |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Other audiences |
| Results and Impact | This was an afternoon event organised for scientists across nine departments of the university: Computer Science, Electronic Engineering, Physics, Chemistry, Environment, Music, Law, Philosophy, and Mathematics. We presented our work, and as a result created a network of scientists in robotics at York. |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://www.york.ac.uk/yorrobots/ |
| Description | women+@DCS seminar on Software Engineering for Robotics |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Postgraduate students |
| Results and Impact | This activity supports the effort at the University of Sheffield to engage women in science. |
| Year(s) Of Engagement Activity | 2021 |
| URL | https://sites.google.com/sheffield.ac.uk/womendcs/ |