SureSwarm

This proposal investigates the verification of designs, for Cyber Physical Systems, against a system of systems

requirement of swarming without collision in the presence of non-determinism due to individual system

failures and the environment in which the systems operate. The cost of verification versus the capability of the

communicating designs (which reflects the performance of the swarm) will be assessed. The issue of scalability

in terms of the number of systems in the swarm and the size of the area they operate in will also be

investigated. Such swarming behaviour can be harnessed to execute a task in the presence of uncertainty. The

verification will be addressed by the use of compositional techniques and a powerful model checker. The

investigation will use a case study of an algorithm for robot swarming in order to introduce failures non-

deterministically and compensate for these by enhancing the algorithm with fault tolerance strategies.

Environmental constraints will be explored through a combination of model checking and efficient robot

simulation techniques.