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. This is on-going R&D and we expect to be able to demonstrate this in flying examples by end 2019.
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.