A Formal Development Approach for Self-Organising Systems

Self-organising systems are distributed systems which achieve an ordered global state without centralised control. They include adaptive sensor networks, swarm robotic systems and mobile ad-hoc networks. Designing such systems is difficult and often based on a trial-and-error approach. In this paper, we provide an approach which is both systematic and formal. Our approach builds on the formalism of Object-Z and the refinement approach of action systems. It follows an intuitive approach to development which breaks a refinement proof into three steps which the designer may iterate through on the way to the final design.