Towards a unified methodology for the design and development of distributed control system software

A unified approach to the design and development of distributed control software is presented. This method is the result of a 'tight' integration between a formal method for concurrent systems (CSP) and a structured method for distributed control system (DARTS). The work presented in this thesis does not seek to extend the semantic model of CSP nor to design a specific control algorithm, rather, efforts are made to apply the existing specification and verification techniques to enhance the formality of the well established and case-proven structured counterparts that benefits are captured from both methods. As a methodology is the central aim, the suggested approach is a first step towards a complete unified software development environment, which engineers can follow from organising design ideas to system implementation with proven correctness. The thesis develops a set of parameterised CSP predicates for expressing concurrency and communication together with a corresponding set of generic processes to reflect these specified behaviours. These generic processes are formal building blocks for generating system implementations at different levels of abstraction. Utilisation of DARTS criteria and the parameterised CSP objects frame the refinement strategies. Also, mappings of generic processes to pictorial representations are suggested which enable easy assimilation of the evolving designs. Applicability of the approach is demonstrated through a high level software design of a highperformance robot control system where its suitability is shown via requirement specifications, properties verification and implementation of salient behaviours using generic building blocks. Although verification often means rigorous mathematical reasoning, the thesis presents a proof assistant the Causality Diagram Evaluation Tool to automate the manipulation of CSP processes according to the defined algebraic laws. It is shown to be of value in reasoning with designs and implementations of the robot system. It is found that the analysis facility and the graphical interpretation of communication provided by the tool allow effective analysis and manipulation of early designs. The results derived from specifying essential design details, from transforming highly abstracted implementation models, and from investigation of system behaviours through formal reasoning and simulation conclude that formal methods, in particular CSP, has a niche value in enhancing software reliability at the sub-system level as well as providing a better underpinning to the structured method DARTS. The end product is a method to generate a correct and unambiguous document of the system concerned that is amenable to a direct implementation.