Automated verification and validation
Official Title: Automated Verification and Validation for Defence, Aerospace and Automotive Embedded Software
QinetiQ’s Systems Assurance Group (SAG) collaborated with Bill Roscoe’s group at Oxford from the early 1990s on the use of research from Oxford such as Communicating Sequential Processes (CSP) and the verification tool FDR. SAG applied these to MOD projects, assessing the dependability of software systems, such as Plug & Play Weapons architectures and Eurofighter avionics, up until 2012. In 2012, core people from SAG set up the company D-RisQ. D-RisQ obtained a license from QinetiQ enabling them to take the technology forward to commercialise it. A key part of their work concentrates on making the sophisticated FDR verification tool accessible to engineering practitioners through automated analysis of formalisms such as SysML and Stateflow.
The exploitation is continuing through D-RisQ Ltd to analyse automotive architectures and for entry level autonomy for an Unmanned Air Vehicle. Oxford and D-RisQ are collaborating on the DARPA-funded HACMS programme, working on the security of autonomous vehicles. Funding from this project is playing an important part in the development of FDR3, the new version of FDR.