132301SureSwarmClosedFeasibility StudiesInnovate UKThis 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.