A Calculus for Software Engineering of Mobile and Autonomous Robots
Lead Research Organisation:
University of York
Department Name: Computer Science
Abstract
The basic mathematical principles that guide the engineering of software are, by far and large, known. The techniques whose notations and procedures are justified by these principles are called formal methods, and it is just relatively recently that main players in industry like Microsoft have started using formal methods to improve the quality of their products. What is routine in many engineering disciplines is just now becoming feasible for software developers.
The practical use of formal methods in many specific areas of application is still an open challenge that is being tackled by scientists and engineers worldwide. In RoboCalc, we face this challenge in the exciting area of development of controller software for mobile and autonomous robots. Our focus is on the development of formal methods with applicability in this industry.
This requires pushing the boundaries of the state of the art in two respects. Firstly, we have to contribute for the further development of the foundations of software engineering. We need to cope with models of the physical environment in which robots operate; the environment has a direct impact on the behaviour of the controller. We also need to cope with timed and probabilistic behaviours, which are exhibited both by the environment and the controllers themselves. Finally, we need to characterise and understand the languages and design techniques used for simulation and programming of robot controllers. All this needs to be considered in an integrated and consistent way. The second important aspect of the work to be carried out is the design of procedures and tools to support the automated application of the novel techniques; this ensures scalability and usability.
Our vision is a 21st-century toolbox for robot-controller developers. In this toolbox, a developer can find unambiguous diagrammatic notations to specify models for the environment, the robotic platform, and the controller. For commonly used environments and robotic platforms, the toolbox includes a range of ready-made models. Because these models are precise, there is no scope for misunderstanding and, most importantly, the toolbox includes techniques that allow analysis of desirable properties of the models: deadlock freedom, speed limits, and so on.
A technique for validation that robot controller developers favour nowadays is simulation. In the 21st-century toolbox, there are tools for automatic generation of these simulations. The ingenuity of the developer is now focussed in the optimisation of the simulation and of the associated deployed code. These optimisations are often needed, and so the toolbox also includes facilities to ensure that changes maintain compliance with the models previously developed. Moreover, because the languages used for simulation and programming are high-level, the results are tool independent, and can be deployed in a variety of robotic platforms.
All this is in stark contrast with current practice. Nowadays, typically, high-level models are either informal or not really of a high level, as they are described in a programming language. With these models, facilities for analysis is limited. Simulations and deployments evolve independently, and so any reasoning has to be at the (tool and hardware dependent) code level.
With the 21st-century toolbox, the costly cycles of iterations of design and testing, with problems found very late, even just at deployment time, are reduced. Moreover, the developer can demonstrate that the controller produced satisfies essential properties established during modelling. Software for mobile and autonomous robot is cheaper and more reliable.
The 21st-century toolbox has been made possible because the calculus for the engineering discipline for robot-controller software is understood and put into practice. This is our goal in RoboCalc.
The practical use of formal methods in many specific areas of application is still an open challenge that is being tackled by scientists and engineers worldwide. In RoboCalc, we face this challenge in the exciting area of development of controller software for mobile and autonomous robots. Our focus is on the development of formal methods with applicability in this industry.
This requires pushing the boundaries of the state of the art in two respects. Firstly, we have to contribute for the further development of the foundations of software engineering. We need to cope with models of the physical environment in which robots operate; the environment has a direct impact on the behaviour of the controller. We also need to cope with timed and probabilistic behaviours, which are exhibited both by the environment and the controllers themselves. Finally, we need to characterise and understand the languages and design techniques used for simulation and programming of robot controllers. All this needs to be considered in an integrated and consistent way. The second important aspect of the work to be carried out is the design of procedures and tools to support the automated application of the novel techniques; this ensures scalability and usability.
Our vision is a 21st-century toolbox for robot-controller developers. In this toolbox, a developer can find unambiguous diagrammatic notations to specify models for the environment, the robotic platform, and the controller. For commonly used environments and robotic platforms, the toolbox includes a range of ready-made models. Because these models are precise, there is no scope for misunderstanding and, most importantly, the toolbox includes techniques that allow analysis of desirable properties of the models: deadlock freedom, speed limits, and so on.
A technique for validation that robot controller developers favour nowadays is simulation. In the 21st-century toolbox, there are tools for automatic generation of these simulations. The ingenuity of the developer is now focussed in the optimisation of the simulation and of the associated deployed code. These optimisations are often needed, and so the toolbox also includes facilities to ensure that changes maintain compliance with the models previously developed. Moreover, because the languages used for simulation and programming are high-level, the results are tool independent, and can be deployed in a variety of robotic platforms.
All this is in stark contrast with current practice. Nowadays, typically, high-level models are either informal or not really of a high level, as they are described in a programming language. With these models, facilities for analysis is limited. Simulations and deployments evolve independently, and so any reasoning has to be at the (tool and hardware dependent) code level.
With the 21st-century toolbox, the costly cycles of iterations of design and testing, with problems found very late, even just at deployment time, are reduced. Moreover, the developer can demonstrate that the controller produced satisfies essential properties established during modelling. Software for mobile and autonomous robot is cheaper and more reliable.
The 21st-century toolbox has been made possible because the calculus for the engineering discipline for robot-controller software is understood and put into practice. This is our goal in RoboCalc.
Planned Impact
The potential impact of the work we propose is far reaching, given the large number of prospective and current applications of mobile and autonomous robots. Benefit to society is going to be realised, in the longer term, via the increased safety and lower cost of the robotic systems developed with the use of our techniques. For example, autonomous vehicles can become widespread, with uses for entertainment, surveillance, defense and so on, and industrial robots can become more interactive and cooperate with humans.
In more detail, we note the following non-academic beneficiaries:
* general public, who will have another tool to understand the abstract concepts of Computer Science and Software Engineering;
* developers, who will have modern tools to tackle the difficult problem of programming robot controllers;
* certifiers, who will have techniques for program verification, and can reasonably request from developers the artefacts that provide evidence of properties of the robot controllers, with traceability provided to link designs, simulations, and deployments;
We expect the impact on the general public to be achieved during the lifetime of the project and beyond, on developers at the end of the project, and on certifiers in the longer term.
We note that our approach is based on state machines, a notation well accepted by engineers. In addition, we eagerly pursue automation. This addresses scalability, but also accessibility of techniques and results. Impact is, in this way, improved, from the point of view of developers and certifiers.
The multitude of applications of robots that can become economically viable mean that, indirectly, our results can support cultural enrichment (with robots used in museums, galleries and libraries), quality of life (with robots used in domestic cleaning activities), health (with robots used in home-care setups), environmental protection (with robots used for pollution monitoring). On a more technical vein, our results can provide evidence that safety cases can be made for mobile autonomous robots. This can influence governmental and industrial guidelines both in the UK and internationally. In the case of businesses involved in robot development themselves, our results will generate the knowledge that they can use to significantly improve their design, validation, and verification skills. With the growth expected in the market, the impact will be significant, and attract and optimise investment.
While some of our research assistants will concentrate on the scientific foundations of the engineering of robot-controller software, some will have just the right skills to work in the modern robotics industry. Undergraduate and MSc students will also benefit from our results, since our demonstrators and examples can be incorporated in modules on software engineering and robotics.
According to market reports, the UK software industry is on the rise and is presently the second largest market by value in Europe. The UK has expertise in the development of safety-critical software in a wide number of domains. The state-of-the-art technology that we will developed will further enhance this expertise, and help us to maintain significant international leadership. The UK has clear international leadership in formal methods. This project will help us maintain our position. We will ensure our continued presence in a very important section of the society.
In more detail, we note the following non-academic beneficiaries:
* general public, who will have another tool to understand the abstract concepts of Computer Science and Software Engineering;
* developers, who will have modern tools to tackle the difficult problem of programming robot controllers;
* certifiers, who will have techniques for program verification, and can reasonably request from developers the artefacts that provide evidence of properties of the robot controllers, with traceability provided to link designs, simulations, and deployments;
We expect the impact on the general public to be achieved during the lifetime of the project and beyond, on developers at the end of the project, and on certifiers in the longer term.
We note that our approach is based on state machines, a notation well accepted by engineers. In addition, we eagerly pursue automation. This addresses scalability, but also accessibility of techniques and results. Impact is, in this way, improved, from the point of view of developers and certifiers.
The multitude of applications of robots that can become economically viable mean that, indirectly, our results can support cultural enrichment (with robots used in museums, galleries and libraries), quality of life (with robots used in domestic cleaning activities), health (with robots used in home-care setups), environmental protection (with robots used for pollution monitoring). On a more technical vein, our results can provide evidence that safety cases can be made for mobile autonomous robots. This can influence governmental and industrial guidelines both in the UK and internationally. In the case of businesses involved in robot development themselves, our results will generate the knowledge that they can use to significantly improve their design, validation, and verification skills. With the growth expected in the market, the impact will be significant, and attract and optimise investment.
While some of our research assistants will concentrate on the scientific foundations of the engineering of robot-controller software, some will have just the right skills to work in the modern robotics industry. Undergraduate and MSc students will also benefit from our results, since our demonstrators and examples can be incorporated in modules on software engineering and robotics.
According to market reports, the UK software industry is on the rise and is presently the second largest market by value in Europe. The UK has expertise in the development of safety-critical software in a wide number of domains. The state-of-the-art technology that we will developed will further enhance this expertise, and help us to maintain significant international leadership. The UK has clear international leadership in formal methods. This project will help us maintain our position. We will ensure our continued presence in a very important section of the society.
Organisations
- University of York (Lead Research Organisation)
- D-RisQ (Collaboration)
- Aarhus University (Collaboration)
- Universidade de São Paulo (Collaboration)
- Southwest University (Collaboration)
- Newcastle University (Collaboration)
- Transport Systems Catapult (Collaboration)
- Microsoft Research (Collaboration)
- Trinity College Dublin (Collaboration)
- Simomics Ltd (Collaboration)
- Praxis Systems Ltd (Collaboration)
- University of Ulster (Collaboration)
- University of Bremen (Collaboration)
- Federal University of Pernambuco (Collaboration)
- Indian Institute of Science Bangalore (Collaboration)
- Fudan University (Collaboration)
Publications
Divakaran S
(2015)
Formal Methods and Software Engineering
Cavalcanti A
(2015)
Test selection for traces refinement
in Theoretical Computer Science
Nielsen C
(2015)
Systems of Systems Engineering Basic Concepts, Model-Based Techniques, and Research Directions
in ACM Computing Surveys
Woodcock J
(2015)
Editorial
in Formal Aspects of Computing
Foster S
(2015)
Mechanised Theory Engineering in Isabelle
Ye K
(2015)
Model checking of state-rich formalism by linking to $$CSP\,\Vert \,B$$ C S P ? B
in International Journal on Software Tools for Technology Transfer
Cavalcanti A
(2015)
Theoretical Aspects of Computing - ICTAC 2015
| Description | The goal of our work is the development of a 21st-century toolbox for robot-controller developers. The development of this toolbox and its scientific underpinnings are well under way. We already have a framework for with unambiguous diagrammatic notations to specify models for the robotic platform and the controller. Because these models are precise, there is no scope for misunderstanding and, most importantly, the toolbox includes techniques that allow analysis of desirable properties of the models: deadlock freedom, speed limits, and so on. We cater for both timed and probabilistic properties. A technique for validation that robot controller developers favour nowadays is simulation. In the 21st-century toolbox, there are tools for automatic generation of these simulations. The ingenuity of the developer is now focussed in the optimisation of the simulation and of the associated deployed code. Since the languages used for simulation are high-level, the results are tool independent, and can be deployed in a variety of robotic platforms. Because of the automation, we have usability and scalability. |
| Exploitation Route | The outcomes of this project are being taken forward in a variety of pathways to impact: additional funding attracted (from EPSRC and RAEng), and take up in industry is under way. Industrial interest nationally and internationally is leading to technology transfer activities funded by industry. |
| Sectors | Aerospace, Defence and Marine,Agriculture, Food and Drink,Chemicals,Digital/Communication/Information Technologies (including Software),Electronics,Environment,Healthcare,Leisure Activities, including Sports, Recreation and Tourism,Manufacturing, including Industrial Biotechology,Culture, Heritage, Museums and Collections,Retail,Transport |
| URL | https://robostar.cs.york.ac.uk/ |
| 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 RoboCalc 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). |
| 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 | Distinguished Visiting Fellow DVF (Round 4) |
| Amount | £2,865 (GBP) |
| Funding ID | DVF1516\4\23 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 06/2016 |
| End | 07/2016 |
| 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 Standard Grant |
| Amount | £1,776,973 (GBP) |
| Funding ID | EP/R025479/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 04/2018 |
| End | 03/2023 |
| 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 | Hazardous Scene Assessment |
| Amount | £78,500 (GBP) |
| Organisation | Defence Science & Technology Laboratory (DSTL) |
| Department | Centre for Defence Enterprise |
| Sector | Public |
| Country | United Kingdom |
| Start | 02/2017 |
| End | 06/2017 |
| Description | Horizon 2020 |
| Amount | € 7,000,000 (EUR) |
| Organisation | European Commission |
| Sector | Public |
| Country | European Union (EU) |
| Start | 01/2015 |
| End | 12/2017 |
| Description | Newton Research Collaboration Programme |
| Amount | £23,374 (GBP) |
| Funding ID | NRCP1617/6/164 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 01/2017 |
| End | 12/2017 |
| Description | Newton Research Collaboration Programme |
| Amount | £23,105 (GBP) |
| Funding ID | NRCP1617/5/68 |
| Organisation | Royal Academy of Engineering |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 08/2016 |
| End | 10/2017 |
| 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 | TSB Open Call |
| Amount | £22,000 (GBP) |
| Organisation | Innovate UK |
| Sector | Public |
| Country | United Kingdom |
| Start | 04/2016 |
| End | 03/2017 |
| 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 | 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 | Chemical Agent Detection |
| Organisation | Ulster University |
| Department | Faculty of Life and Health Sciences |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Development of a hardware demonstrator of a neural network based control system for chemical agent detection. Using the tools developed in RoboCalc we will explore the limits of what is possible to model with respect to a complex controller based on neural networks. |
| Collaborator Contribution | They are experts in the development of hardware based neural networks. |
| Impact | Funded grant from the CDE (phase 1 development of prototype) |
| Start Year | 2016 |
| 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 with Fudan University |
| Organisation | Fudan University |
| Country | China |
| Sector | Academic/University |
| PI Contribution | We have begun very early work on the application of the tools developed in the project to case studies being undertaken by researchers at Fudan. We visited once in 2018 (Sept) and plan to visit again later this year and work with MSc and PhD students in more detail. We have provided insight into the use of the tools and suggested possible application areas. |
| Collaborator Contribution | They have provided outline case studies for us to examine, so that we can focus work for 2019. |
| Impact | At this stage, outcomes are limited, expect the development of a plan for 2019 work. |
| Start Year | 2018 |
| 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 | D-RisQ |
| Organisation | D-RisQ |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Development of a case study, the alpha algorithm, using the techniques for modelling and simulation developed in the project. As a result of a our joint efforts, we have evolved both our reserch and their product. |
| Collaborator Contribution | Development of a case study, the alpha algorithm, using the techniques for modelling and simulation used in their company. As a result of a our joint efforts, we evolved both our reserch and their product. |
| Impact | * A case study, including two models, several simulations. * Improvements to D-RisQ's tools. * Improvements to our notation to deal with collections of robots. * Improvements to our simulation approach. |
| Start Year | 2016 |
| 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 | INTO-CPS collaboration |
| Organisation | Aarhus University |
| Country | Denmark |
| Sector | Academic/University |
| PI Contribution | Collaboration between EU Horizon 2020 project and RoboCalc. RoboCalc contributed to a new work item in INTO-CPS on adding new languages and tools to the INTO-CPS toolchain. Specifically, the probabilistic version of RoboChart and its translation to the PRISM model checker. |
| Collaborator Contribution | Work carried out by investigator funded by INTO-CPS project. |
| Impact | Draft publications. |
| Start Year | 2017 |
| Description | INTO-CPS collaboration |
| Organisation | Newcastle University |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Collaboration between EU Horizon 2020 project and RoboCalc. RoboCalc contributed to a new work item in INTO-CPS on adding new languages and tools to the INTO-CPS toolchain. Specifically, the probabilistic version of RoboChart and its translation to the PRISM model checker. |
| Collaborator Contribution | Work carried out by investigator funded by INTO-CPS project. |
| Impact | Draft publications. |
| Start Year | 2017 |
| Description | Mota UFPE |
| Organisation | Federal University of Pernambuco |
| Country | Brazil |
| Sector | Academic/University |
| PI Contribution | Collaboration on probabilistic aspects of RoboChart language: semantics, examples, tools. |
| Collaborator Contribution | Collaborative work on probabilistic RoboChart. |
| Impact | Draft publications. |
| Start Year | 2017 |
| Description | Partnership in the application of RoboChart |
| Organisation | Fudan University |
| Country | China |
| Sector | Academic/University |
| PI Contribution | Training for use of RoboChart |
| Collaborator Contribution | Explaining the potential collaborative research area of RoboChart |
| Impact | No. |
| Start Year | 2019 |
| 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 | Testing from Circus with Mealy Machines |
| Organisation | Universidade de São Paulo |
| Department | Institute of Mathematical and Computer Sciences (ICMC) |
| Country | Brazil |
| Sector | Academic/University |
| PI Contribution | Expertise on model-based testing based on process algebras and resfinement. |
| Collaborator Contribution | Expertise on testing based on Mealy machines. |
| Impact | Joint papers |
| Start Year | 2015 |
| 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 | 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 | 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 |
| Title | Automated Verification of Reactive and Concurrent Programs by Calculation, supporting material |
| Description | Abstract Event-driven reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber physical systems and autonomous robots, and so verification support for them is highly desirable. We present a verification strategy for concurrent and 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, and parallel composition, which allows flexible specification of various concurrency schemes. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) semantic framework, which provides soundness guarantees, and practical verification support.
Isabelle Formalisation This archive accompanies the JLAMP journal submission, "Automated Verification of Reactive and Concurrent Programs by Calculation". All of the Isabelle/HOL theories needed to support the theorems developed in this paper are included, and also the dependencies from the Archive of Formal Proofs (AFP). This development depends on Isabelle/2019 (from https://isabelle.in.tum.de/). In order to view the theories, you first need to make Isabelle aware of the Isabelle/UTP directly. You can either do this by adding a reference to its absolute path in the ROOTS file of your Isabelle installation, or else by invoking Isabelle on the command line with a command such as:
|
| Type Of Technology | Software |
| Year Produced | 2019 |
| Open Source License? | Yes |
| URL | https://zenodo.org/record/3541079 |
| Title | Automated Verification of Reactive and Concurrent Programs by Calculation, supporting material |
| Description | Abstract Event-driven reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber physical systems and autonomous robots, and so verification support for them is highly desirable. We present a verification strategy for concurrent and 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, and parallel composition, which allows flexible specification of various concurrency schemes. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) semantic framework, which provides soundness guarantees, and practical verification support.
Isabelle Formalisation This archive accompanies the JLAMP journal submission, "Automated Verification of Reactive and Concurrent Programs by Calculation". All of the Isabelle/HOL theories needed to support the theorems developed in this paper are included, and also the dependencies from the Archive of Formal Proofs (AFP). This development depends on Isabelle/2019 (from https://isabelle.in.tum.de/). In order to view the theories, you first need to make Isabelle aware of the Isabelle/UTP directly. You can either do this by adding a reference to its absolute path in the ROOTS file of your Isabelle installation, or else by invoking Isabelle on the command line with a command such as:
|
| Type Of Technology | Software |
| Year Produced | 2019 |
| Open Source License? | Yes |
| URL | https://zenodo.org/record/3541080 |
| Title | RoboToool |
| Description | RoboTool provides a graphical editor for models written in a domain-specific language for robotics, RoboChart. RoboTool also generates automatically mathematical definitions that capture the behaviour of the RoboChart model, and is integrated with a model checker. This is a tool that is able to use the mathematical definitions to prove properties like freedom of deadlock and livelock. Instead of testing the system or the model, a model checker explores exhaustively all the states of the model to ensure that the property of interest is satisfied in all states. Using the definition generated by RoboTool, we can also prove specific properties of a robotic system, like impossibility of ignoring a particular event in given circumstances, for example. If, however, the property does not hold, a model checker provides a counterexample. RoboTool is provided as a set of Eclipse plugins implemented using the Xtext 1 and Sirius 2 frameworks. Xtext automatically generates plugins that implement a parser, and provides mechanisms for the implementation of validators, type checkers, and code generators, for instance. Sirius supports the definition of graphical representations, and produces a plugin for construction and visualisation of models. The model checker used by RoboTool is FDR4. |
| Type Of Technology | Software |
| Year Produced | 2016 |
| Open Source License? | Yes |
| Impact | General interest in academia and industry in using the results of our project. |
| URL | https://www.cs.york.ac.uk/circus/RoboCalc/robotool/ |
| Description | A demonstration of probabilistic modelling and verification in RoboTool to researcher in University of Agder |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | Demonstrated the probabilistic modelling and verification in RoboTool through PRISM to colleagues in the University of Agder on February 26th 2020 via Skype. Audiences include researcher and master students. At the same time, Pedro demonstrated RoboTool in general. To prepare for this demo, an online resource (see https://robostar.cs.york.ac.uk/prob_case_studies/probabilistic_verification_tutorial/index.html) was created. |
| Year(s) Of Engagement Activity | 2020 |
| Description | BCS FACS Evening Seminar |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | The BCS Specialist Group for practitioners in Formal Aspects of Computing Science has members drawn from both industry and academia. It acts as a bridge between the two communities, helping British industry to stay in the forefront of formal computer techniques, and British academics to maintain the applicability of their research. It arranges informal seminars to encourage technology transfer throughout the year: about four a year. |
| Year(s) Of Engagement Activity | 2016 |
| URL | http://www.bcs.org/content/ConWebDoc/56123 |
| 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 | 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 | 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 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 | Isabelle/UTP Tutorials in Southwest University, Chongqing, China |
| 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 | This tutorial lasted for two afternoons, covers three main topics: functional programming with Isabelle/HOL, imperative programming with Isabelle/UTP, and reactive programming with Isabelle/UTP. The material of the tutorial is very much based on the tutorial that Dr. Simon Foster gave during CyphyAssure Spring School. |
| Year(s) Of Engagement Activity | 2019 |
| URL | http://computer.swu.edu.cn/s/computer/kxyj2xsky/20190509/3706486.html |
| 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 | Present "Engineering Robotic Swarms" in the Pint of Science at 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 | Presented at Pivni of York from 7:30 PM - 9:30 PM on May 22, 2019, with James Baxter and Richard Redpath (Jon Timmis). Abstract Robots are becoming part of our everyday lives, from making cars and cleaning the house to assisting with surgery and exploring areas too dangerous for humans to enter. But can we trust them to be safe? In this talk, we look at ways that Mathematics, Computer Science, and Software Engineering can play a part to ensure that robots behave in the way we expect them to. We discuss groups of robots working together and the problems and solutions related to working with them. We show the power of these techniques lives in action. Using frogs. And the audience. What could possibly go wrong? |
| Year(s) Of Engagement Activity | 2019 |
| URL | https://pintofscience.co.uk/event/-blurred-lines-boundaries-between-man-and-machine |
| 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 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 | Presented "Modelling and verification of probabilistic behaviour of robotic applications" during a two-day workshop to communicate with our visitors (Prof. Zhiming Liu and his team) from Southwest University |
| 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 | Agenda: 1. Overview of RoboChart; 2. Background of reactive modules, PRISM and MDP; 3. How to transform models from RoboChart to PRISM; 4. Verification support through PRISM and the assertion language in RoboTool; 5. Example and performance. Date: Jul 23, 2019 9:30 AM - 11:00 AM Location: University of York This talk was presented during a two-day workshop to communicate with our visitors (Prof. Zhiming Liu and his team) from Southwest University, Chongqing, China. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Public lecture |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Public/other audiences |
| Results and Impact | Short lecture on the interaction between biology and robotics and the need to develop safe robotic systems that can interact with humans and the environment. |
| Year(s) Of Engagement Activity | 2017 |
| 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 | RoboCheck |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Postgraduate students |
| Results and Impact | About 40 research students attended a school organised in York. Afterwards, several students showed interest in our project and our interests. We have discussed ideas for further work. |
| Year(s) Of Engagement Activity | 2015 |
| URL | https://www.cs.york.ac.uk/circus/RoboCalc-event/ |
| 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 | 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 | School visit (London) |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Schools |
| Results and Impact | Prof Timmis gave a series of talks to years 10 and 12 students at St, Michael's College, Burmonsea, London. The talks were around the use of robotics and their limitations and issues around safety. In addition, he talked about careers in the subject area. |
| Year(s) Of Engagement Activity | 2019 |
| 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 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 | 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 | 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 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 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 | Workshop for academics and industrialists in Pernambuco, Brazil |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | A workshop organised by the Federal University of Pernambuco, Brazil, to present our project and their own experiences in robotics, ranging from support technology development, participation in competitions, to actual deployment of systems. In attendance were academics and students from the local Centre of Informatics, other departments interested in applications, and the local industry. RoboCalc, its results and its goals, were extensively discussed. |
| Year(s) Of Engagement Activity | 2017 |
| Description | Workshop for industry |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Industry/Business |
| Results and Impact | Workshop involving key industry players in robotics. Discussions influenced our work and created opportunities for further collaboration. |
| Year(s) Of Engagement Activity | 2015 |
| URL | https://www.cs.york.ac.uk/circus/RoboCalc/2015/11/Kick-off-meeting |
| 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 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/ |