RoboTest: Systematic Model-Based Testing and Simulation of Mobile Autonomous Robots

Lead Research Organisation: University of Sheffield
Department Name: Computer Science


Mobile and autonomous robots have an increasingly important role in industry and the wider society; from driverless vehicles to home assistance, potential applications are numerous. The UK government identified robotics as a key technology that will lead us to future economic growth ( They have recognised, however, that autonomous robots are complex and typically operate in ever-changing environments ( How can we be confident that they perform useful functions, as required, but are safe?

It is standard practice to use testing to check correctness and safety. The software-development practice for robotics typically includes testing within simulations, before robots are built, and then testing of the actual robots. Simulations have several benefits: we can test early, and test execution is cheaper and faster. For example, simulation does not require a robot to move physically. Testing with the real robots is, however, still needed, since we cannot be sure that a simulation captures all the important aspects of the hardware and environment.

In the current scenario, test generation is typically manual; this makes testing expensive and unreliable, and introduces delays. Manual test generation is error-prone and can lead to tests that produce the wrong verdict. If a test incorrectly states that the robot has a failure, then developers have to investigate, with extra cost and time. If a test incorrectly states that the robot behaves as expected, then a faulty system may be released. Without a systematic approach, tests may also identify infeasible environments; such tests cannot be used with the real robot. To make matters worse, manual test generation limits the number of tests produced.

All this affects the cost and quality of robot software, and is in contrast with current practice in other safety-critical areas, like the transport industry, which is highly regulated. Translation of technology, however, is not trivial. For example, lack of a driver to correct mistakes or respond to unforeseen circumstances leads to a much larger set of working conditions for an autonomous vehicle. Another example is provided by probabilistic algorithms, which make the robot behaviour nondeterministic, and so, difficult to repeat in testing and more difficult to characterise as correct or not.

We will address all these issues with novel automated test-generation techniques for mobile and autonomous robots. To use our techniques, a RoboTest tester constructs a model of the robot using a familiar notation already employed in the design of simulations and implementations. After that, instead of spending time designing simulation scenarios, the RoboTest tester, with the push of a button, generates tests. With RoboTest, testing is cheaper, since it takes less time, and is more effective, because the RoboTest tester can use many more tests, especially when using a simulation.

To execute the tests, the RoboTest tester can choose from a few simulators employing a variety of approaches to programming. Execution of the tests also follows the push of a button. Yet another button translates simulation to deployment tests. So, the RoboTest tester can trace back the results from the deployment tests to the simulation and the original model. So, the RoboTest tester is in a strong position to understand the reality gap between the simulation and the real world.

The RoboTest tester knows that the verdicts for the tests are correct, and understands what the testing achieves; for example, it can be guaranteed to find faults of an identified class. So, the RoboTest tester can answer the very difficult question: have we tested enough?

In conclusion, RoboTest will move the testing of mobile and autonomous robots onto a sound footing. RoboTest will make testing more efficient and effective in terms of person effort, and so, achieve longer term reduced costs.

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 Systems Engineering;
* developers, who will have modern tools to tackle the difficult problem of verifying 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 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 testing of robotic systems, 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 systems 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. Interest in verification of cyber-physical systems in general in Europe and the US is evidenced by a recent report, on the need for EU-US collaboration in modelling and simulation for CPS ( The state-of-the-art technology that we will developed will further enhance this expertise, and help us to maintain significant international leadership.

As a group, we have a strong track record of promoting impact of our research. This covers interaction with the general public and industry. In the group, we have a previous RAEng Enterprise Fellow, a previous RS Industry Fellow, a CEO and a Director of two spin-out companies, and a winner of a Queen's Award for Technological Achievement. This is over and above very successful academic records. We will pursue all pathways to impact available to us for RoboTest.

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/R025134/1 31/03/2018 01/09/2018 £610,060
EP/R025134/2 Transfer EP/R025134/1 02/09/2018 30/08/2024 £575,877
Description We have introduced a novel approach that maps a model of a robotic model, written in our timed and probabilistic state-machine language RoboChart, to a mathematical model (a semantics). RoboChart models are first mapped to CSP, with this providing the potential to utilise standard (and mature) tools that have been developed for CSP. We have shown how a resultant CSP model can be mapped to a mathematical description that can be used as the basis for testing. For this, we required a new approach because the standard mapping to a mathematical model is unsuitable since it does not appropriately account for the differences between inputs and outputs (in testing, the tester controls inputs, the system controls outputs).

A second piece of work introduced novel notions of correctness (implementation relations) for use with models of robotic systems, where these models include timing requirements (e.g. a certain event must happen within a given time). The challenge here was to appropriately reflect the way simulation packages operate so that the implementation relation can be used to support testing within a simulation. We have shown how these implementation relations relate to the standard implementation relations reported in the literature.

We have also developed an automated approach that generates test cases from a RoboChart model. The test cases returned provide guarantees with respect to fault detection; they are guaranteed to reveal certain potential faults. The test cases generated by this approach can be used for testing within a simulation and later we will be exploring approaches that convert them into test cases for the deployed robotic system. The automated technique utilises mutation and is supported by prototype tools.

To improve the quality of the tests generated, we require information about the operational requirements of a robotic system. We have, therefore, developed a controlled natural language, RoboChart, to specify these requirements. With a discretised version of the RoboChart semantics, we have already produced a prototype tool that eliminates useless tests. A medium-size demonstrator of the whole test generation approach is available: an autonomous segway. We are working on a real case study: a fire fighting UAV. RoboChart, however, has a hybrid semantics, and we are working on tool support to allow the improvement of the test generation techniques.

Work on testing with hardware in the loop has been significantly affected by the pandemic. We are progressing with the development of testing infrastructure for simulation-based testing. From RoboChart models, we can generate automatically simulation models and code. Integration with the test-generation technique is upcoming.

In addition, we have shown how one can minimise a given set of tests within our semantics. This work primarily aims to produce a smallest set of tests that is guaranteed to find all faults. However, the techniques developed can also be used to eliminate redundancy in a given set of tests while retaining their effectiveness.

We have worked on semantics and techniques for testing probabilistic models in RoboChart. Our three techniques are:

1. Probabilistic model checking. We developed a translator from RoboChart to Reactive Modules, the input language for the Prism, Storm, and iscasMC probabilistic model checkers.

2. Statistical model checking. Our translation from RoboChart to Reactive Modules enables statistical model checking in Prism (neither Storm nor iscasMC are currently statistical model checkers).

3. Deductive reasoning. We have a variety of semantics for deductive reasoning and we have been exploring which is most tractable in Isabelle/UTP. A tractable semantics is the first step towards a principled theory of probabilistic testing.
Exploitation Route To drive the automated systematic testing of software for robotic systems within simulation. There is also the potential to adapt these test cases, that are designed for simulation, to form test cases for deployed robotic systems. We have worked on the following four semantics:

i) Translation from RoboChart to Probabilistic CSP. Our work uses an early version of the model checker for CSP that has support for probabilistic CSP: FDR2. The work is reported in the paper:

Madiel S. Conserva Filho, R. Marinho, Alexandre Mota, Jim Woodcock: Analysing RoboChart with Probabilities. SBMF 2018: 198-214.

ii) Translation from RoboChart to probabilistic total correctness contracts. This work is reported in the paper:

Jim Woodcock, Ana Cavalcanti, Simon Foster, Alexandre Mota, Kangfeng Ye: Probabilistic Semantics for RoboChart - A Weakest Completion Approach. UTP 2019: 80-105.

We have implemented the total correctness semantics in Isabelle/UTP and we report this in the paper:

Kangfeng Ye, Simon Foster, Jim Woodcock: Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving. RAMiCS 2021: 465-482.

iii) Translation from RoboChart to timed probabilistic predicative relations. This is current work reported in the technical report:

Jim Woodcock: Uncertainty and Probabilistic UTP. Technical Report. 30th September 2021 (35pp).

iv) A Bayesian version of this semantics. This is reported in the technical report:

Jim Woodcock: Semantics of Probabilistic Programming: A subjective Bayesian approach. Technical Report. 14th October 2021 (23pp).
Sectors Aerospace, Defence and Marine,Transport

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 two years now. We have also developed new material for 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 on the effort. Colleagues in academia are also building on our work to develop their own research independently. A couple of examples are reported in
Sector Aerospace, Defence and Marine,Transport
Impact Types Societal

Description FDR models for the SEFM 2021 paper "Checking Opacity and Durable Opacity with FDR" 
Type Of Technology Software 
Year Produced 2021 
Open Source License? Yes  
Description FDR models for the SEFM 2021 paper "Checking Opacity and Durable Opacity with FDR" 
Type Of Technology Software 
Year Produced 2021 
Open Source License? Yes  
Description Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
Description Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
Description Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
Description Royal Academy of Engineering event on Software Engineering for Robotics (RoboSoft). 
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 Two day event on software development for robotic systems. Speakes and audience were a mixture of industry and academia.
Year(s) Of Engagement Activity 2019