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 that enables 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) 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 2 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.
In agreement with our project partners Callen-Lenz, we developed a LRE which takes over from normal path planning/navigation, 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 a 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 satisfies the SRS through the use of a mathematical check. This provides evidence to support the 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.
Looking into the future
The project will be exploited in a number of ways in various sectors. The work has spawned a similar project but this time focussed on the underwater domain. The project showed that the techniques were viable; all we needed to agree on were the behavioural rules.
"The function of good software is to make the complex appear to be simple"