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.

Publications

10 25 50
publication icon
Cavalcanti A (2020) Inputs and Outputs in CSP A Model and a Testing Theory in ACM Transactions on Computational Logic

publication icon
Cengiz Türker U (2021) Minimizing Characterizing sets in Science of Computer Programming

publication icon
Doherty S (2022) Unifying Operational Weak Memory Verification: An Axiomatic Approach in ACM Transactions on Computational Logic

publication icon
El-Fakih K (2021) $\mathcal k$-branching uio sequences for partially specified observable non-deterministic fsms in IEEE Transactions on Software Engineering

publication icon
Hierons R (2019) FSM quasi-equivalence testing via reduction and observing absences in Science of Computer Programming

 
Description We have introduced 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, with this providing the potential to utilise 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).

A second piece of work introduced novel notions of correctness include 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.

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

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.

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. A number of the underlying concepts are also being used to devise an 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).

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. This includes work that has looked at automated systematic testing based on RoboChart models that include inputs, outputs and discrete time. For this, we have test generation algorithms that return is guaranteed to find any faults presence. We have also devised a mutation-based approach, allowing one to target particular faults - this aids scalability.

For probabilistic models, 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 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 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 "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 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. 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...
 
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...
 
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 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 "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 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 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 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