| dc.description.abstract | The subject of this thesis pertains to coordination in systems of entities characterised by mobile, real-time
behaviour and unreliable communication over a wireless network. Such systems are now being deployed both in academic trials and in real-world scenarios towards the achievement of various goals e.g. search and rescue, surveillance, object tracking, traffic management. Coordinating the behaviour of entities in these systems is a non-trivial task, due to real-time demands, sensor inaccuracies, wireless coverage unreliability and entity mobility, among other concerns. A coordination model is a theoretical framework for the development of strategies by which systems of entities can operate safely towards the achievement of their goals. Comhordú is a coordination model that facilitates the definition of scenarios consisting of a number of entities and a safety constraint. Furthermore, it provides a means of deriving behavioural constraints upon entities such that the safety constraint in a scenario is respected while entities pursue their goals. However, there is no formal proof that this is the case. Moreover, the presentation of Comhordú is not formal and is somewhat fragmented, based mostly on a mixture of prose and UML diagrams. Hence there is a need for its formalisation. There are several benefits to formalising a model. A formal specification avoids the ambiguities often implicit in a natural language description. Also, through the process of formalising a model, often necessary modifications or improvements to the original design become apparent. Furthermore, a formal specification can be subjected to rigorous mathematical analysis, often with the aid of a computer. This work is the first to address the formalisation of Comhordú. The goal is to produce a formal specification of Comhordú along with a verification of its correctness with respect to maintaining safety. That is, for every scenario that can be developed with Comhordú, are the coordination strategies sufficient to guarantee that safety for that scenario is maintained? Preceding a formal specification of Comhordu, critical analysis of the original model is provided. This analysis uncovers a number of ambiguities in the original model and argues that certain aspects of the original model would be difficult to formalise. Following this analysis, modifications are made to the original model
yielding a revised model that is more amenable than the original to the process of formalisation. These modifications alone are significant contributions of this work. In light of the modifications made, it is necessary to validate this revised model against the original. That is, the revised model is analysed in how closely it matches the original model. In particular, this analysis focuses on elements from the original that are altered or even wholly absent in the revised model. The revised model is formally specified using a novel formal specification language, developed specifically for the purpose of this work. This language incorporates a general behavioural model for systems of mobile, real-time entities with unreliable wireless communication. Within this language, a protocol is specified; this is based on the idea of behavioural constraints from the original presentation of Comhordu. A proof is provided that this protocol is correct with respect to maintaining safety; roughly speaking the proof says that adherence to the protocol by all entities in a system implies safety in that system. The exact notion of safety is defined later in this thesis. The aforementioned formal specification and proof are encoded using the proof assistant Coq. The language
and protocol description are encoded in Gallina, the specification language of Coq. The proof of correctness is partially translated into Coq. That is, the main theorem pertaining to safety is proved in terms of a number of lower level results, some of which are assumed without proof in the machine encoding. For those results left unproved in Coq, sketch proofs are provided by hand. Overall, then, this work achieves the following. The Comhordu model is modified to produce a revised model, which is validated against the original. The revised model is formally specified by means of a novel formal specification language and a term in that language. This formal specification is translated to Gallina,
the language of the proof assistant Coq, and the proof of correctness is partially completed using Coq. | |
