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.

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.
 
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 They may develop and verify their robotic applications using our technology.
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://www.cs.york.ac.uk/circus/RoboCalc/
 
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. 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.
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Cultural,Societal

 
Description Chair in Emerging Technologies
Amount £1,300,000 (GBP)
Organisation Royal Academy of Engineering 
Sector Learned Society
Country United Kingdom
Start 03/2018 
End 02/2028
 
Description Distinguished Visiting Fellow DVF (Round 4)
Amount £2,865 (GBP)
Funding ID DVF1516\4\23 
Organisation Royal Academy of Engineering 
Sector Learned Society
Country United Kingdom
Start 06/2016 
End 07/2016
 
Description EPSRC Standard Grant
Amount £1,776,973 (GBP)
Funding ID EP/R025479/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 04/2018 
End 03/2023
 
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 Newton Research Collaboration Programme
Amount £23,105 (GBP)
Funding ID NRCP1617/5/68 
Organisation Royal Academy of Engineering 
Sector Learned Society
Country United Kingdom
Start 08/2016 
End 10/2017
 
Description Newton Research Collaboration Programme
Amount £23,374 (GBP)
Funding ID NRCP1617/6/164 
Organisation Royal Academy of Engineering 
Sector Learned Society
Country United Kingdom
Start 01/2017 
End 12/2017
 
Description RAEng Brazil 1
Amount £24,000 (GBP)
Funding ID NRCP1617/5/68 
Organisation Royal Academy of Engineering 
Sector Learned Society
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 Learned Society
Country United Kingdom
Start 01/2017 
End 01/2018
 
Description TSB Open Call
Amount £22,000 (GBP)
Organisation Innovate UK 
Sector Public
Country United Kingdom
Start 04/2016 
End 03/2017
 
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-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 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 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 University of Sao 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 Publications: (1) A. Alberto, A. L. C. Cavalcanti, M.-C. Gaudel, and A. Simao. Formal mutation testing for Circus. Information and Software Technology, 81:131--153, 2017. (2) A. L. C. Cavalcanti and A. Simao. Fault-based testing for refinement in CSP. In N. Yevtushenko, A. R. Cavalli, and H. Yenigün, editors, 29th IFIP WG 6.1 International Conference on Testing Software and Systems, volume 10533 of Lecture Notes in Computer Science, pages 21--37. Springer, 2017.
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 No outputs yet.
Start Year 2017
 
Description bangalore-2018 
Organisation Indian Institute of Science
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
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 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 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 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 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 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 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 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 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 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 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 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