Verification of the safety of Robotic systems operating in close proximity to Humans
Robotics systems have been evolving for well over 30 years. The car industry adopted robotic systems on production lines which automated various dangerous and repetitive tasks and various parts of the nuclear and indeed space industry have done likewise for decades.
However, the environment in which of robotics systems have been used has been very tightly constrained and the possibility of harm to humans consequently has been very low. In order to make wider use of robotics, there has to be an assurance that they are safe; in this era, this also implies that they are also secure. This is because there is likely to be a much closer engagement with humans.
The sectors range from aerospace, medicine to help in the home. Given that requirements for safety and security can be established, showing that they meet these requirements cost effectively is very difficult. The vast majority of the functionality will be vested in software (or complex electronics such as FPGAs) and will naturally have to incorporate decision making in order to be useful. Demonstrating that a robotics system is safe under all circumstances of use is therefore challenging. Without meeting this challenge, the wide scale adoption of robotics systems cannot realistically happen where public safety is at risk.
The typical approach to the development of software based systems has a cost profile heavily weighted towards the end of the project; this represents considerable project risk. Robotics systems will have to be resilient to user interaction and may have to interact with other systems, maybe over the internet. The production of evidence should drive the selection of the best development life cycle, processes and tools. The production of verification evidence through either review, analysis or test to provide assurance of resilience should be a by-product of the use of such development techniques and be responsive to inevitable change as understanding increases though the development process. The testing based approach cannot be exhaustive and cannot be cost effective. The only realistic solution is to use mathematical proof through the use of formal methods in order to reduce the test burden.
The use of formal methods can be used to provide analysis for both architectures and software. To date, it has been assumed that experts are required to write formal specifications by hand and then to prove the necessary properties using appropriate qualified tools as support. This is not necessarily a quick or repeatable process and where in other industries formal techniques have been used, they have become company specific knowledge, not available to the wider community. Therefore in order for formal techniques to be adopted more widely across industry, they need to be automated in order to achieve the required flexibility, repeatability, have a low training overhead, as well as providing evidence of resilience.
D-RisQ has taken an approach which enables the power of formal methods to be exploited without any specialist training. By using commonly available tools such as Stateflow®, it is now possible for current engineers to develop software systems architectures in a rigorous manner, whilst gaining as a by-product, the required evidence to confidently support system release.
Modelworks® proves that requirements have been correctly captured in a design expressed in Stateflow®, or will show the manner in which compliance has failed. The design can be of a System of Systems, a single system or a software program. It allows a designer to check that the design does what is required. More importantly, it allows a proof that undesired properties will never happen, a check that is typically attempted at the end of a development life-cycle. It is also possible to show behaviour under failure conditions. Modelworks can be used to show the behaviour of highly distributed Systems-of Systems, including the behaviour of human interaction where necessary.
CLawZ® automatically proves that automatically produced code implements a design expressed in Simulink®. By using the ADI Ada auto-coder or the TargetLink® C auto-coder aligned to the Simulink control system subset, CLawZ® produces evidence that the code correctly implements the design, or shows where the coder has made a mistake. This relieves the need to undertake unit testing thus gaining considerable time benefits.