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

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

Abstract

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 (tinyurl.com/q8bhcy7). They have recognised, however, that autonomous robots are complex and typically operate in ever-changing environments (tinyurl.com/o2u2ts7). 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 (https://www.steinbeis-europa.de/files/tams4cps-srac_e-book_01-2017_1.pdf). 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.
 
Description 1. A novel approach that maps a robot control-software model, written in our timed and probabilistic state-machine language RoboChart, to a mathematical model (a semantics) using a notation called CSP.

RoboChart models are first mapped to CSP, enabling standard (and mature) tools for verification. 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).

2. Novel notions of correctness, including timing requirements (such as, 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.

3. 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.


4. A controlled natural language, RoboWorld, to specify operational requirements of a robotic system.

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 firefighting UAV. RoboChart, however, can be connected to physical models of the robot and environment, which, together, have a hybrid semantics. We are now working on tool support to allow the improvement of the test generation techniques that use a widely adopted middleware for robotics, ROS.



5. Testing infrastructure for simulation-based testing.
From RoboChart models, we can generate automatically simulation models and code. We have also developed a technique that allows one to convert a test case generated from the original (timed) RoboChart model into a test for use in simulation.


A technique to minimise a given set of tests.
This work produces 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. The initial work was for a semantics in which there could be no internal (unobservable) actions and this has been generalised to allow such internal actions.

6. Automated test generation algorithm that allows one to return a finite test suite that is complete in the sense that it finds all faults given a standard test hypothesis (an upper bound on the number of system states).

Ongoing work is extending both the test minimisation and test generation algorithms to a timed setting.


Semantics and techniques for testing probabilistic models in RoboChart. Our three techniques are:

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

b. 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).

c. 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 1. Tool developers may want to adapt or extend their tools to implement our techniques. We are working with an industrial partner in that respect.

2. Software developers may want to adapt their techniques to take advantage of the RoboTest approach. We are working with an industrial partner to consider their hardware as a target for our simulations and tests.

3. RoboTest is part of the more general RoboStar framework with support for simulation and proof. RoboTest techniques, however, have provided results that are particularly useful for industry. So, software developers may want to adopt the whole RoboStar collection of notations and techniques. We are working with an industrial partner with that in view.

4. Roboticists struggle with the use of ROS in the context of systems that need to be trustworthy. Our techniques can inform developers on best practice in terms of design approach.
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 an audience more focused on science and engineering, but still generalist, we have written popular articles, given webinars, and published a podcast. We have also developed new material for YorkTalks (https://www.york.ac.uk/research/events/yorktalks/). We have material ready and are developing more material to engage in this form of activity. As a result, we have also trained the Research Assistants in dealing with the public. We are engaging with industry nationally and internationally to train human resources and support the development of new tools. Colleagues in industry are also leading the effort. T. Lecomte, D. Déharbe, P. Fournier, M. Oliveira: The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199, 102524 (2020). reports on efforts by industry to provide support for use of RoboTest technology in their safety platform. Another current effort is providing support for implementation of RoboTest results in a prized testing tool adopted by major players in the cyber-physical industry. An incoming Royal Academy of Engineering Fellowship is pursuing technology transfer by extending the result to deal with humans in the loop. Colleagues in academia are also building on our work to develop their own research independently. An example is reported in W. Lindoso, S. C. Nogueira, R. Domingues, L. Lima: Visual Specification of Properties for Robotic Designs. In: S. Campos and M. Minea (eds.) Formal Methods: Foundations and Applications - 24th Brazilian Symposium, SBMF 2021, Virtual Event, December 6-10, 2021, Proceedings. pp. 34-52. Springer (2021). Finally, we are engaging with potential users through presentations at Sheffield Robotics events.
Sector Aerospace, Defence and Marine,Transport
Impact Types Societal

 
Title Dataset for Paper "Digital twin based testing for cyber-physical systems: A systematic literature review" 
Description An excel spreadsheet containing exported metadata collected during a systematic literature review on digital twin based testing for cyber-physical systems. 
Type Of Material Database/Collection of data 
Year Produced 2022 
Provided To Others? Yes  
URL https://figshare.shef.ac.uk/articles/dataset/Dataset_for_Paper_Digital_twin_based_testing_for_cyber-...
 
Title Dataset for Paper "Digital twin based testing for cyber-physical systems: A systematic literature review" 
Description An excel spreadsheet containing exported metadata collected during a systematic literature review on digital twin based testing for cyber-physical systems. 
Type Of Material Database/Collection of data 
Year Produced 2022 
Provided To Others? Yes  
URL https://figshare.shef.ac.uk/articles/dataset/Dataset_for_Paper_Digital_twin_based_testing_for_cyber-...
 
Title Implementing and Verifying Release-Acquire Transactional Memory (Artifact) 
Description Supplementary files for the paper "Implementing and Verifying Release-Acquire Transactional Memory". The upload includes: Isabelle/HOL files for all proofs. The proofs have been developed/tested on Isabelle/HOL 2021-1. C++ implementations of TML-SC and TML-RA 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
URL https://zenodo.org/record/6899918
 
Title Isabelle/HOL files for "Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies" 
Description Isabelle/HOL files for the paper "Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies". Tested for Isabelle 2022. 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
URL https://figshare.com/articles/software/Isabelle_HOL_files_for_Mechanised_Operational_Reasoning_for_C...
 
Title Isabelle/HOL files for "Ownership-Based Owicki-Gries Reasoning" 
Description Isabelle/HOL files for "Ownership-Based Owicki-Gries Reasoning" accepted to SAC 2023. The theories have been tested on Isabelle 2022. 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
URL https://figshare.com/articles/software/Isabelle_HOL_files_for_Ownership-Based_Owicki-Gries_Reasoning...
 
Title Tamarin Models for "Verifying List Swarm Attestation Protocols" 
Description Tamarin models and proofs of SIMPLE+ and its variations for the paper "Verifying List Swarm Attestation Protocols" to appear in WiSEC 2023. https://doi.org/10.1145/3558482.3581778 The proofs have been tested with Tamarin 1.6.1. 
Type Of Technology Software 
Year Produced 2023 
Open Source License? Yes  
URL https://figshare.com/articles/software/Tamarin_Models_for_Verifying_List_Swarm_Attestation_Protocols...
 
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  
URL https://figshare.com/articles/software/FDR_models_for_Checking_Opacity_and_Durable_Opacity_with_FDR_...
 
Description Isabelle/HOL files for "Unifying Operational Weak Memory Verification: An Axiomatic Approach" to appear in ACM Transactions on Computational Logic. The proofs require Isabelle/HOL 2020. 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
URL https://figshare.com/articles/software/Isabelle_HOL_files_for_Unifying_Operational_Weak_Memory_Verif...
 
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  
URL https://figshare.com/articles/software/Isabelle_files_for_View-Based_Owicki-Gries_Reasoning_for_Pers...
 
Description Keynote at LOPSTR 2022 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Public/other audiences
Results and Impact Gave a keynote at the 32nd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2022). The title of the keynote was "Systematic Software Testing for Robotics".
Year(s) Of Engagement Activity 2022
URL https://lopstr2022.webs.upv.es/#speakers
 
Description Presentation at Sheffield Robotics day - with external visitors and collaborators 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Industry/Business
Results and Impact This was a talk at an open one day event held by Sheffield Robotics: the annual Sheffield Robotics Showcase. Participants include researchers from across the university, researchers from Sheffield Halam (also a member of Sheffield Robotics), industrial collaborators, and health professions. The puprose was to provide an overview of the Verifiability Node, outline the work being carried out at Sheffield, and encourage collaboration.
Year(s) Of Engagement Activity 2022
 
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
 
Description Talk at Sheffield Robotics 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Professional Practitioners
Results and Impact Short presentation to describe the Verifiabiltiy Node and the TAS programme, outline the work to date at Sheffield, explain our plans, and encourage collaboration.
Year(s) Of Engagement Activity 2022