SeaSwarm

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.