The Challenge
Whilst it is possible to generate behaviour in an single autonomous vehicle that does what is required, it is really difficult to show that it won’t do what is not required – ever – particularly where safety is needed. It is also possible to show that a collection of vehicles will operate together, but it is very difficult to show that they will always do this in all circumstances, let alone show that unwanted behaviour is absent.
How can such required behaviours be described such that not only developers can usefully use it, that regulators can understand it and verification of the eventual development can be quickly and easily verified? Furthermore, can we avoid a statistical approach to safety assurance which is generally deemed to be insufficient to support a safety case.
Assuring the Behaviour of a Single Vehicle - BVLOS
Introducing Kapture® & Modelworks®
While AI, machine learning and risk based control for vehicles can be very good, there is not yet a practical way of assuring their behaviour. However, D-RisQ has developed a technique of assuredly bounding the behaviour of such systems through automatic formal proof.
We described the required behaviour of an autonomous Unmanned Air Vehicle (UAV), which was to be in accordance with the rules-of-the-air, using English and used the D-RisQ tool Kapture® to ensure that these requirements were verifiable. We then showed that the design expressed in Simulink satisfied these requirements using D-RisQ Modelworks® automatic verification tool.
This approach can therefore enable a UAV to fly Beyond Visual Line of Sight(BVLOS), with suitable sensing, and is a foundation for assuring swarming behaviour. This was flown by our project partner Callen-Lenz and the UAV behaved exactly as expected.
Assuring a Swarm
Now we can express the behavioural requirements for a swarm, or cooperating vehicles, in English using D-RisQ Kapture®. What we need to know is the rules for the swarm and what it means to be able to achieve the set task and hence to be able to maintain swarm coherence. This is then taken to the design stage and expressed in Simulink®/Stateflow®. Each vehicle than has this extra functionality added and we then check the whole swarm behaviour using Modelworks®.
Scalability and Certification
We often get asked how scalable is this technique? The foundation work was built on a 2D grid and we used cloud resources to tackle the 20 Billion or so states in about 90 minutes. Using inductive techniques we showed that it was theoretically possible to assure an arbitrary size swarm.
Now tackling 3D problems, we have examples that show that we can assure a swarm of 6 UAVs operating in a 10x10x10 grid within 10 mins and for 8 UAVs within 20 mins using a laptop (note: the grid can move, it’s the relationship between the vehicles that matters). We can speed this up by using cloud computing.
From a certification/safety case perspective, we have used DO-178C/DO-333 as the basis for all our work. We have developed verifiable requirements and automatically shown that the design satisfies these. We then will use and autocoder to produce C code and will automatically formally verify it using D-RisQ CLawZ® and in due course will automatically formally verify the object code using D-RisQ FEVER® thus giving compliance to the majority of the verification Objectives in DO-333.
