Abstract
Swarm robotics has been proposed as a way to organise decentralised systems in which a large number of similar robots, that are autonomous and relatively simple in their behaviour, are coordinated in a way that leads to an emergent useful behaviour. The Cooperative Cleaners case study is an example of swarm robotics. In this case study, a group of robots cooperate in order to reach the common goal of cleaning a dirty floor. A cleaning robot has a bounded amount of memory; it can only observe the state of the floor in its immediate surroundings and decide on its movement based on these observations. The cleaning robots use indirect communication based on sensing and signalling, and the desired goal of cleaning the whole floor is thus an emergent behaviour of the swarm. In this thesis we show how the Cooperative Cleaners case study can be modelled and analysed using the Real-Time ABS language. Real-Time ABS is a timed, abstract and behavioural specification language with a formal semantics and a Java-like syntax that targets concurrent, distributed and object- oriented systems. We use the features of Real-Time ABS in the development of our model of the Cooperative Cleaners problem in order to evaluate how well Real-Time ABS can be used to model and analyse the behaviour of systems from the swarm robotics domain. Our work shows that Real-Time ABS can facilitate the modelling of these kinds of systems, but due to the challenges introduced when formally modelling systems in this domain, it requires fairly advanced modelling skills to obtain an adequate model. However the analysis of these kinds of systems is currently restricted to simulations applied to small scenarios.