D-RisQ Modelworks®

The Challenge

Beyond Visual Line of Sight operations for Unmanned Air Vehicles can only realistically be undertaken if the aircraft can operate fully autonomously in accordance with the rules-of-the-air (i.e. SERA), especially where collision avoidance is concerned.

A human cannot be expected to react in time, in all circumstances over a link, as the time delay alone may mean that an accident may have already happened. Something else has to be on board, ready to take over when short notice collision avoidance is needed. In order to be able to design the software for such a system a modelling approach is required, enabling verification that the design satisfies the requirements and should support platform certification.

Architecture and Safety Case

An architecture that took sensor data into a ‘Last Response Engine’ (LRE) and which gave instructions to the autopilot needed to be developed. Sensor data was to be supplied in this case solely by ADS-B; sensing could be provided by any other set of sensors as the basis for decision making.

Requirements would need to be formalised in the D-RisQ Kapture® tool and used as the basis for development of the design; this would mean that requirements were verifiable. It was agreed that there should be two major iterations of the design which would have firstly, some basic functionality and then some more advanced capabilities, that would exhibit ‘airmanship’. The safety case was to be based upon compliance to the Standardised European Rules of the Air (SERA) for collision avoidance.

A volume around the UAV was established for a ‘safety bubble’ and requirements were based on a clearly expressed context that would encompass numerous use cases. The software development from system requirements to design would need to be in accordance with DO-178C acceptable practices, utilising the Formal Methods Supplement DO-333.

Solution

In agreement with our project partners Callen-Lenz, we developed a LRE which takes over from normal path planning/navigation, and commands an avoidance action in accordance with SERA. The behavioural rules were expressed in English and written up in a System Requirements Document (SRD).

This was transformed into a Software Requirements Specification (SRS) which was written in the D-RisQ Kapture® tool. This was automatically transformed into formal semantics, i.e. a language that could be used for automatic verification. A review was conducted to assure that the SRS accurately and completely captured the SRD. A design was developed in Simulink/Stateflow to reflect the SRS. This design complied with the subset of Simulink/Stateflow used by Modelworks®.

The use of Modelworks® exhaustively checks that the design satisfied the SRS through the use of a mathematical check. This provides evidence to support a safety case and hence platform certification. Successful air trials were held throughout the project where one UAV with the decision-making system was flown at another without it; no collisions were observed it always behaved as expected by another air user.