auto_awesome_motion View all 1 versions
organization

D-RisQ Ltd

Country: United Kingdom
9 Projects, page 1 of 2
  • Funder: UKRI Project Code: EP/S001190/1
    Funder Contribution: 562,549 GBP
    Partners: D-RisQ Ltd, ClearSy, United Technology Research Center UTRC, University of York

    This research concerns assuring safety of autonomous robots. A robot is a machine that is capable of performing a complex sequence of steps, in order to achieve some goal. Autonomous robots act independently and do not require the direct intervention of a human operator. For example, autonomous vehicles are cars, lorries, or other road vehicles that are able to drive themselves to a destination without the need for a human driver. Another example are robot carers, that are able to assist elderly or disabled people with every day tasks, such as retrieving items, cleaning, playing games, and so on. Autonomous robots therefore present a number of exciting future opportunities for overcoming societal challenges. Robots are computer systems, and the software that runs on them is very complex, far more so than a typical desktop, laptop computer, or mobile phone. Such computers have very simple inputs, like keyboard, mouse, and touchscreen. Robots, however, are "cyber-physical systems": they are both computational (cyber) devices, but they also interact with their physical environment. They have both sensors, that allow them to "see", "hear", and "feel" the world, and also actuators which allow them to manipulate objects in the world. For example, a care robot may have arms that it can move, and wheels to move around with. The software as a robot therefore has to be constantly monitoring its environment, and be able to quickly, appropriately, and, most importantly, safely respond to the changing environment. If we cannot guarantee that a robot carries out its tasks safely, we cannot risk using them, as human injury or even death could result. A recent example concerns a Tesla Model S automated car that was unable to see a large white lorry crossing its path, and ploughed into the side of it killing its driver. Such tragic accidents reveal why safety is an utmost concern. Our research will employ mathematical and logical techniques in an attempt to demonstrate that a robot is safe to operate in its target environment. We will employ a document called a "safety case" that contains a credible and convincing safety argument. This argument must, of course, be supported by evidence, and our technique will provide this through "model-based design", where computerised models of individual system parts are created as virtual prototypes. Such models can be described using complicated mathematics, such as algebra, differential equations, and probabilistic models. Probability, in particular, is very important since robots need to plan for possible uncertainty in there environment - such as a human being in an unexpected place. Mathematics allows us to be rigorous - considering a large range of possible scenarios that would be very expensive to test in the real world. However, it is also difficult for a human to do the necessary mathematics manually. We will therefore use software called an "automated theorem prover" to try and show that each of the robot models behaves correctly and safely. This will include new techniques specifically for reasoning about cyber-physical systems. We will apply our new techniques to a number of industrial problems, gleaned from our a number of robotics companies that we will partner with. This will allow us to provide guidance to them in ensuring their systems are safe. Our hope is that ultimately our project will ensure that robots can be safely introduced into our society, and thus open up a host of exciting future business opportunities.

  • Funder: UKRI Project Code: EP/R025134/2
    Funder Contribution: 575,876 GBP
    Partners: INTEL Corporation SAS, Blue Bear Systems Research Ltd, Verified Systems International GmbH, University of Liverpool, ESC (Engineering Safety Consultants Ltd), Liverpool Data Research Associate LDRA, Adelard, BRL, Federal University of Pernambuco, D-RisQ Ltd...

    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.

  • Funder: UKRI Project Code: EP/R025134/1
    Funder Contribution: 610,059 GBP
    Partners: Federal University of Pernambuco, University of Liverpool, Liverpool Data Research Associate LDRA, Brunel University, Adelard, D-RisQ Ltd, ESC (Engineering Safety Consultants Ltd), BRL, Blue Bear Systems Research Ltd, INTEL Corporation SAS...

    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.

  • Funder: UKRI Project Code: EP/K040251/1
    Funder Contribution: 1,157,930 GBP
    Partners: Technology Dev Group BioDundee, D-RisQ Ltd, SU, MONO, Lemma 1, DECC, MICROSOFT RESEARCH LIMITED, IBM (United Kingdom), UWO, LMS...

    Mathematics is a profound intellectual achievement with impact on all aspects of business and society. For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. "Crowdsourcing" pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers check proofs that are just too long and complicated for any human to comprehend, using programs designed to verify hardware. Yet these techniques are currently used in stand-alone fashion, lacking integration with each other or with human creativity or fallibility. Social machines are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity. Our long-term vision is to change mathematics, transforming the reach, pace, and impact of mathematics research, through creating a mathematics social machine: a combination of people, computers, and archives to create and apply mathematics. Thus, for example, an industry researcher wanting to design a network with specific properties could quickly access diverse research skills and research; explore hypotheses; discuss possible solutions; obtain surety of correctness to a desired level; and create new mathematics that individual effort might never imagine or verify. Seamlessly integrated "under the hood" might be a mixture of diverse people and machines, formal and informal approaches, old and new mathematics, experiment and proof. The obstacles to realising the vision are that (i) We do not have a high level understanding of the production of mathematics by people and machines, integrating the current diverse research approaches (ii) There is no shared view among the diverse re- search and user communities of what is and might be possible or desirable The outcome of the fellowship will be a new vision of a mathematics social machine, transforming the reach, pace and impact of mathematics. It will deliver: analysis and experiment to understand current and future production of mathematics as a social machine; designs and prototypes; ownership among academic and industry stakeholders; a roadmap for delivery of the next generation of social machines; and an international team ready to make it a reality.

  • Funder: UKRI Project Code: EP/K040251/2
    Funder Contribution: 1,146,390 GBP
    Partners: Lemma 1, MONO, MICROSOFT RESEARCH LIMITED, IBM (United Kingdom), JacobsUni, University of Oxford, D-RisQ Ltd, UWO, Institute of Mathematics and its Applica, SU...

    Mathematics is a profound intellectual achievement with impact on all aspects of business and society. For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. "Crowdsourcing" pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers check proofs that are just too long and complicated for any human to comprehend, using programs designed to verify hardware. Yet these techniques are currently used in stand-alone fashion, lacking integration with each other or with human creativity or fallibility. Social machines are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity. Our long-term vision is to change mathematics, transforming the reach, pace, and impact of mathematics research, through creating a mathematics social machine: a combination of people, computers, and archives to create and apply mathematics. Thus, for example, an industry researcher wanting to design a network with specific properties could quickly access diverse research skills and research; explore hypotheses; discuss possible solutions; obtain surety of correctness to a desired level; and create new mathematics that individual effort might never imagine or verify. Seamlessly integrated "under the hood" might be a mixture of diverse people and machines, formal and informal approaches, old and new mathematics, experiment and proof. The obstacles to realising the vision are that (i) We do not have a high level understanding of the production of mathematics by people and machines, integrating the current diverse research approaches (ii) There is no shared view among the diverse re- search and user communities of what is and might be possible or desirable The outcome of the fellowship will be a new vision of a mathematics social machine, transforming the reach, pace and impact of mathematics. It will deliver: analysis and experiment to understand current and future production of mathematics as a social machine; designs and prototypes; ownership among academic and industry stakeholders; a roadmap for delivery of the next generation of social machines; and an international team ready to make it a reality.