Unmanned Systems Technology 002 | Scion SA-400 | Commercial UAV Show report | Vision sensors | Danielson Trident I Security and safety systems | MIRA MACE | Additive manufacturing | Marine UUVs

61 Security and safety systems | Insight industry. A recent report by McKinsey for the UK’s Innovate UK r&d agency showed that the overall market for global robotics, which includes autonomous systems, will be $1.26tn by 2025 but that a key barrier is showing the technology is safe, and the key barrier for that is cost. Adding application security test and verification increases the cost unless it is built in from the start of the process. Part of the way to do that is to automate the design tools. If they can be certified for automatic test and verification then developers can take certification credit for the use of that tool in whichever standards process is being used. This then highlights the importance of automatic code generation, proof and formal methods, and has been adopted in new, higher-level design approaches such as the Unified Model Language (UML) and System-level Model Language (SysML). The executable code generated automatically has to be shown as a full and correct implementation of the requirements, which can be costly. An alternative method is to use a formal proof, which can show the absence of a behaviour (which you can’t do with a test) and can assess the responses under multiple failures, including when under attack. There can then be a mathematical demonstration from requirements to object code to show the formal correctness of the result. Tools such as medina, from IKV Technologies, can take SysML and UML models as well as Simulink models developed specifically for ISO 26262 automotive designs to integrate functional safety analysis and development activities. It supports safety analysis and design for software-controlled, safety- related functions with risk and hazard analysis methods – including hazard list, risk graph, fault tree analysis and failure mode and effects analysis with the modelling and code generation tools from MathWorks. But moving to new architectures such as agents means autonomous systems need a more complex verification environment, so a project was set up in January 2015 to take high-level models in the SysML language and use a formal model checker called FDR3 (developed at the University of Oxford) that implements parallel processing to explore autonomous software designs for stability, reaching all the different states automatically through a tool called ModelFlow, from D-RisQ. At the moment, the translation of the properties is done by hand, which is problematic and could be prone to errors, so the next step is to ensure those properties are carried over from the SysML models to the model checker automatically and correctly. This allows the model checker to demonstrate that the design meets the requirements. Conclusion The move to autonomous systems is challenging the testing and verification of software from both the safety and security perspectives. New architectures such as rational agents aim to simplify the test and verification process, and at the same time reduce the attack surface for malicious software, making systems less prone to hacking. All of this requires more automation in the design tools, moving development up from the level of the source code to sophisticated yet flexible models of autonomous behaviour. Taking these models and automatically generating code and verification dramatically reduces the overhead of certification and so makes system development more cost-effective. It also gives the flexibility to support different standards across different applications while demonstrating appropriate levels of safety and security. Acknowledgements The author wishes to thank Nick Tudor of D-RisQ Systems, the UK’s Safety Critical Systems Club, Mike Bartlett of Test and Verification Solutions, Jeremie Guichet of the University of Toulouse, Ireri Ibarra of MIRA, Michael Fisher of the University of Liverpool, Richard Parris of Intercede and Andrew Ashby of Plextek Consulting for their input into this article. Unmanned Systems Technology | Spring 2015 The University of Oxford’s FDR3 tool for checking the requirements of safety code