Drisq Ltd Public Funding

Within safety and security critical systems, a measure of sufficient test is Modified Condition/Decision Coverage (MC/DC). Constructing a sufficient set of test cases in order to achieve this MC/DC metric requires considerable time and expense and often delays project acceptance and commercial release. We propose to develop a mechanism for the automatic production of just such a set of test cases that can be formally proven to meet MC/DC criteria. Combining the expertise from D-RisQ (UK) Newcastle University (UK) and Fortiss (GE) with the testing knowledge from Verified International (GE) as well as the knowledge from partners in aerospace, automotive, medical devices as well as nuclear regulation, we intend to ensure that results are compatible with regulators needs by meeting the relevant standards.

This 5-month collaborative feasibility study will identify potential cyber and safety vulnerabilities with current small boat (<150 kW) electric propulsion and control technologies and then develop a roadmap which outlines tools and techniques to assess and address these vulnerabilities going forward. This is important work to allow the scaling of decarbonisation technologies in the maritime industry. This feasibility study will: * Undertake cyber security testing at the University of Plymouths (UoP) Cyber Ship Lab on a representative electric propulsion and control system * Benchmark the system and software against accepted software safety practices using an innovative formal method approach developed by D- RisQ Ltd * Develop tools, techniques and a future roadmap outlining the steps necessary to achieve high levels of cyber and safety assurance in such products going forward * Present a future trial to demonstrate the proposed techniques and assurance processes applied to an electric propulsion/control system operating in a representative operational environment The move towards electrification, digitisation and autonomy in the marine sector is exposing what have previously been simple closed, isolated mechanical systems to ones that are increasingly dependent on software and external connectivity. This makes them increasingly vulnerable to various threat vectors in terms of digital cyber security and safety. Cyber security and safety assurance will be a critical element in exploiting the rapidly emerging marine electrification market (currently £4.5Bn/yr+), particularly with government users and large corporations or safety critical markets. By assessing the vulnerability of current systems and providing a structured and assured approach to the development of such systems and software, benchmarking against existing industry standards for safety and cyber-security, we will be able to produce a roadmap that shows how to develop safe and secure smart shipping systems going forward This project brings together a partnership of experienced academics and established businesses: * RAD Propulsion will lead the project and provide a representative electric propulsion and control system for assessment. * The UoP has extensive autonomy, maritime and cyber security research expertise, operates its own fleet of vessels/USVs and will contribute its innovative Cyber Ship Lab test facilities to the project. * D-RisQ will bring expertise in high integrity software development and testing for both safety and security, applying its innovative formal method techniques which it developed for use in other domains Stehr Consulting Ltd brings specialist experience of maritime regulatory and certification frameworks to support identification of relevant cyber and safety standards and potential regulatory/certification barriers.

Within aerospace and other industries, it is widely recognised that poor requirements are the root cause of cost overruns in systems development and, in thankfully rare cases, accidents after a system has been deployed. The aim of this project is to significantly reduce the opportunity for error in writing system requirements thus reducing cost and helping to avoid accidents. We aim to provide a means for the typical systems engineer to easily write clear, concise, unambiguous system requirements which can then be used as a sound basis for use in future verification activities. The technology will exploit a mathematical technique called 'Formal Methods'. We will provide a set of templates that enable a systems developer to write English language requirements thus enabling stakeholders such as regulators, developers and testers to clearly understand the intent.

Demeter uses energy-harvesting, intelligent, uncrewed vehicles to provide a persistent, infrastructure-independent subsea sensor data retrieval and analysis service. It is a compelling alternative to CAPEX-heavy fixed power and communication networks that would otherwise be required to support the widespread use of subsea sensors and systems for long-term monitoring of asset health, thus accelerating subsea digitalisation. Demeter will enable more cost-effective predictive maintenance of subsea assets, greatly reduce OPEX and downtime, and ultimately lower the cost and environmental impact of exploiting renewable and non-renewable offshore resources alike. Downstream, Demeter has further application in maritime security operations, including maritime surveillance. Key innovations include: long-endurance, energy-harvesting, hybrid underwater and surface autonomous vehicles; an onboard edge-processing module based on a novel computer architecture, capable of performing intensive statistical analysis of harvested sensor data at a fraction of the power of current technologies; a technology stack for high-integrity long-term autonomous navigation and decision making; and embedded subsea sensors adapted for data retrieval by the autonomous vehicles. As an integrated solution, Demeter aims to shift the subsea monitoring paradigm from one of manual, expensive, and low-frequency _data_ retrieval to that of automated, inexpensive, high frequency and on-demand _intelligence_ retrieval. Suitably evolved, Demeter will open up entirely new concepts of operation for maritime security that are not currently feasible. The project brings together a diverse set of partners to deliver a game-changing capability: Autonomous Devices, a specialist developer of robotic solutions for extreme and challenging environments; Signaloid, developers of a paradigm-shifting computer architecture for edge computing; D-RisQ, developers of a unique technology stack for the implementation of high integrity autonomous behaviours; CRP Subsea, developers of advanced subsea infrastructure monitoring and engineering products; autonomous mission planning experts from Royal Holloway University of London; autonomous navigation experts from the University of Manchester; and novel marine vehicle design, analysis and testing experts from the University of Strathclyde.

Subsea inspection and surveys require highly accurate mapping to support activities such as site assessment, detailed inspection, and asset maintenance. Data collected can be leveraged through the advancements and application of underwater robotics and autonomous systems to support future industry grow. By improving data accuracy and utility, operational costs and campaign durations can be reduced, eliminating the need for repeat surveys. This supports making offshore a trusted cost efficient and sustainable industry. SEAMless (Subsea Enhanced Autonomous Mapping) will develop a gold standard in composite 3D mapping to deliver the 'Google Maps' of subsea with positioning better than GPS. The fusion of multiple complementary sensors, such as visual perception, novel bio inspired wake detection, acoustic-inertial hybrid navigation, and position sensors, will provide an unambiguous answer to "Where am I?" and "What's around me?". This makes the task of deciding what to do next much easier for autonomous assets and is a key enabler for next-generation trusted long-endurance subsea autonomy. The advanced perception and intelligent decision-making systems will run on-board an autonomous underwater vehicle through a modular architecture. The provision of dense millimetric mapping and drift tolerant positioning, in turn, reinforces the autonomous navigation and control to improve system performance and safety. The latest in serious gaming technologies will provide advanced visualisation, situational awareness and pre-mission planning and post-mission analysis. SEAMless will operate in open water and near infrastructure, for offshore renewables, oil and gas decommissioning and environmental assessments to provided targeted surveys and inspections. This project aims to create a system that could feasibly map an entire offshore windfarm creating a digital model through multiple session, with increased autonomous awareness enabling underwater robots to position themselves and navigate along safe collision free path.

The A2I2 project have been developing untethered, underwater robotic platforms which make unmanned operations the standard for inspection and light intervention tasks for physical infrastructure, primarily in the offshore and nuclear domains. We are developing small, hover-capable Autonomous Underwater Vehicles (AUVs) equipped with a novel visual mapping system and enhanced & verified on-board autonomy. The designs of the platforms are scalable enabling work across domains. They are capable of conducting very close inspection and intervention tasks, such as cathodic protection surveys, coring, visual inspection and metrology and moving small items (e.g. in nuclear ponds). The primary sensing apparatus is Rovco's SubSLAM stereo camera system, with associated computer vision software to allow the creation of 3D maps of the environment. The 3D data serves multiple purposes: enabling safe navigation in complex, cluttered environments by providing a 3D occupancy grid for guidance software; allowing localisation of targets detected by machine learning object recognition; and as metric survey output. To enable the A2I2 robots to manoeuvre safely near sensitive infrastructure, the consortia are addressing current technological limitations: * Perception in cluttered underwater environments * Robust (Fail Safe) operation near sensitive infrastructure * Precision manoeuvring and control near infrastructure * Communication with robots in challenging underwater environments. A2I2 provides a step-change beyond SotA in artificial intelligence control and communications. The consortia members working in the offshore domain (Rovco, NOC and D-RisQ), supported by the Offshore Renewable Energy Catapult, will use this additional funding to demonstrate, verify and validate the system in the offshore operational environment. This will see improvements made to the perception system and the vehicle and would incorporate last response engine software to manage behaviour in the event of connection loss or other critical events. We will develop a safety case for the system and the project will culminate by demonstrating a semi-autonomous survey of an asset (i.e export cable and monopile) with a human in the loop. This is a significant step-change in operational capability. The system will ultimately remove the need for pilot operators to be present on the vessel, as the vehicle requires only supervision which can be conducted remotely. This in turn reduces the costs and environmental impact of operations by allowing smaller, less fuel consuming vessels to be used. The current drive to reduce crew as a direct impact of COVID-19 is accelerating the adoption of remote and autonomous technologies, this follow-on project performs the V&V demonstrations to accelerate the technology to market.

no public description

HICLASS is a project to enable the delivery of the most complex software-intensive, safe and cyber-secure systems in the world. It is a strategic initiative to drive new technologies and best-practice throughout the UK aerospace supply chain, enabling the UK to affordably develop systems for the growing aircraft and avionics market expected over the next decades. It includes key primes, system suppliers, software companies and universities working together to meet the challenge of growing system complexity and size. HICLASS will allow development of new, complex, intelligent and internet-connected electronic products, safe and secure from cyber-attack that can be affordably certified.

Underwater robots are increasingly utilised for commercial and scientific applications to make measurements and interact with the underwater environment. The A2I2 (Autonomous Aquatic Inspection and Intervention) robots will operate in hazardous underwater environments, for offshore renewables, oil and gas, and nuclear applications. Two specific intervention use-cases will be addressed through demonstrators; offshore coring, and wet nuclear storage pond inspections and interactions. These demonstrators are significantly different and therefore enable the project to address multiple market opportunities. This project will address the need for new approaches that are required to permit operation near to critical infrastructure. These will include increased intelligence on the underwater robots to enable them to position themselves and navigate avoiding collision with the surrounding environment.

Enhancing Safety, Reliability and Airworthiness of BVLOS Autonomous UAV operations is a critical element in the development of technology which will allow the safe, routine use of UAV (Drone) technology in the civil environment. The project seeks to bridge the gap between the unmanned and manned aerospace domains, combining the structured approach to "certification" for manned aircraft with the innovation in unmanned aircraft. Through the increase of autonomy in a controlled and validated manner, Unmanned Systems will be able to deliver more capability in the civil environment, reducing hazards for human operations, in particular in demanding inspection environments in fields such as oil and gas, civil engineering and logistics in austere environments.

SECT-AIR’s aims are to develop strategies for the UK high integrity software industry to significantly lower development costs and to scope a UK aerospace software centre-of excellence to maintain these strategies in the future. SECT-AIR plans to define processes and technologies that will make a step change reduction to software development costs; gain adoption of these through certification authorities and wider industry engagement and to ensure a better flow of technology between academia and industry in these areas in the future.

This proposal investigates the verification of designs, for Cyber Physical Systems, against a system of systems requirement of swarming without collision in the presence of non-determinism due to individual system failures and the environment in which the systems operate. The cost of verification versus the capability of the communicating designs (which reflects the performance of the swarm) will be assessed. The issue of scalability in terms of the number of systems in the swarm and the size of the area they operate in will also be investigated. Such swarming behaviour can be harnessed to execute a task in the presence of uncertainty. The verification will be addressed by the use of compositional techniques and a powerful model checker. The investigation will use a case study of an algorithm for robot swarming in order to introduce failures non- deterministically and compensate for these by enhancing the algorithm with fault tolerance strategies. Environmental constraints will be explored through a combination of model checking and efficient robot simulation techniques.

This proposal concerns the verification of a Cyber Physical System (an autonomous sea vehicle) with respect to a requirement for collision avoidance while maintaining swarm behaviour with other autonomous sea vehicles. The work builds upon a D-RisQ case study of verifying collision avoidance requirements for decision making software on-board a sea vehicle for remote unmanned over the horizon operation. The step change is the provision of communication between individual decision making systems to enable emergent swarming behaviour. Such swarming behaviour can be harnessed for search and location. The verification will be addressed by the use of compositional techniques and a powerful model checker that can be run very cheaply on cloud servers in order to scale the exhaustive search through trillions of states. The current limiting factor for modelling swarms is the time taken to compile large models consisting of many parallel components. Oxford University will investigate how compilation can exlpoit multiple cores to speed up compilation, and how lazy compilation can be used to speed-up the compilation of systems containing complex parallel components.

Awaiting Public Project Summary

The USMOOTH project addresses regulatory and safety issues appertaining to unmanned Over The Horizon (OTH) operations of Unmanned Surface Vessels and will develop robust vessel behaviours, reliable communications, situational awareness and a robust safety case. ASV has teamed with; D-RisQ, to introduce from the aerospace domain accredited software development techniques; Cranfield University, to further develop collision avoidance algorithms; safety specialist Frazer Nash Consultancy and the Maritime Coastguard Agency (MCA) to provide safety and regulatory expertise. Success in this project will accelerate UK industrial penetration into offshore energy, scientific and defence markets for tasks such as subsea positioning environmental monitoring and maritime security. The approach is to address USV technologies alongside their human operators introducing a holistic solution to robustly address the safety constraints blocking current USV deployment.

This project seeks to explore the possibility of using automated formal techniques to verify Executable Object Code. If the feasibility study shows that it is, then D-RisQ and Lemma 1 will develop the technology for commercial release. This technology is attractive to the market because the cost of verification is rising dramatically as complexity increases and is particularly attractive to the Robotics and Autonomous Systems market because it will enable the demonstration that the software does only what is required and crucially, never does what is forbidden. The cost of providing such evidence to support a safety case is currently very high. With automated techniques, the cost basis will change substantially and will enable a more rapid, assured development of many types of software systems.

All pieces of self-replicating malware have a signature. However, malware can change form, so the signature of the malware is different even though it has the same destructive behaviour. This means that current techniques will always play catch up with new forms of the same piece of self-replicating malware. By using formal methods to detect the semantics of self-replication, we have the opportunity to detect any self-replicating malware (even if it is unknown or metamorphic) and thus have an opportunity to remove it before any damage can be done. The approach is novel because current techniques detect the signature of malware and then remove it. We have undertaken foundation research to show that we can detect self-replicating behaviour in a sample of obfuscated binary for an ARM processor. Our objective in this project is to expand the applicability and examine scalability.

D-RisQ Ltd and Blue Bear Systems Research Ltd (BBSR) are collaborating on a project called ‘Certifying Autonomy’. The project will develop a maritime based system provided by BBSR that will be subject to validation from a design perspective using technologies developed by D-RisQ to meet the needs of autonomous systems certification. The validation technology is founded on automated formal methods which allow fully exhaustive exploration of design and checking it against textual requirements. The automation is required to reduce cost and enable design engineers regular access to the rigour imposed by the use of formal methods. Using commonly available design tools underpinned by appropriate formal semantics, we can define the boundary of the behaviour of an autonomous system and prove that it conforms to requirements under every normal circumstance. Where possible, we will also involve showing what happens under failure conditions of, for example, other automatic systems or unanticipated environmental inputs. We will explore the certification requirements and also the software implementation of the design and attempt to show how to meet certification requirements for autonomous, software based systems in not only the maritime domain, but ensure that the evidence can be applied to other more challenging domains such as civil aerospace

The project will seek to exploit high end research which indicates that automatic verification of C code generated from modelling languages such as Simulink can be achieved through the use of mathematical proof techniques called Formal Methods. The project's aim is to hide all the maths such that a commercially viable product can ultimately be developed and sold into regulated markets such as Aerospace, Automotive, Cyber and Nuclear. The proof of this concept will unlock further investment funding and enable access to a market worth £100M's well within 5 years.