Semantics of an optional parallel operator for CSP

Abstract

Communicating Sequential Processes (CSP) is arguably one of the most widely used process algebras. It has been extensively studied and expanded since its inception in the late 1970s. One of the fundamental assumptions of parallelism in CSP is that all processes have to jointly engage in synchronised events. There are cases however, especially when Wireless Sensor Networks (WSN) are modelled in CSP, where this restriction constrains the expressive capacity of CSP from a practical perspective. Optional parallelism lifts the restriction of parallelism in CSP by allowing processes to partially engage in synchronisation events. WSNs often have node or communication failures which increases the complexity of the CSP specifications of such WSNs. Basic communication constructs like broadcasting are also difficult to model in CSP, and other process algebras have been developed to allow broadcasting communication. Optional parallelism reduces the complexity by allowing processes to broadcast to other processes as well as to opt out of synchronisation when they are not ready to synchronise. The notion of optional parallelism introduces a new operator to CSP without redefining the semantics of existing operators or the definition of a new process algebra entirely. This dissertation details the design of a translation of the definition of optional parallelism into classical CSP operators which will enable optional parallelism to easily be used in existing CSP model-checkers. The core of the translation entails the addition of a channel modelling artefact to the existing process definitions which allows a communication event between the process and its environment to occur or not. The processes are thus independent from each other with the channel artefacts orchestrating the synchronisation between them. If a process is not ready to engage in an event, its channel ignores the event, and the process essentially opts out of synchronisation. Different combinations of the channel artefacts result in different directional synchronisation cases. Simplex synchronisation has the same behaviour as broadcasting. Duplex communication constructs are also defined which has the same behaviour as bidirectional synchronisation. Focus was given on the operational semantics of optional parallelism in the development of a classical CSP translation. This resulted in a new optional parallel operator being defined with the same operational semantics as the initially defined optional parallel operator. The operational semantics of the new optional parallel operator have been expanded to allow for directional synchronisation which better defines the notion of broadcasting and bidirectional communication links. Two software tools were developed, OptoCSP and OpTrace. OptoCSP provides the functionality to convert CSP system definitions containing the optional parallel operator into CSP definitions containing only classical CSP operators. The software tools developed greatly simplified the trace generation of systems containing the optional parallel operator as this had to be manually scrutinised by hand. OpTrace was used to test for trace refinement between the initial optional parallel definitions and the translation of this dissertation with the use of WSN graph structure definitions. It has a trace generator which has the CSP step laws of the initial optional parallel operator implemented and a model generator which converts the WSN graph structures into CSP models with the new optional parallel translation. The model-checking tool, ProCSP, is used together with OpTrace to perform the trace assertions of the computed traces and the models. OpTrace and ProCSP was used to conclude if the test scenarios presented in this dissertation passed or not. A relationship between the traces of WSN systems defined with the initial optional parallel operator and the translation thereof has been found. This result enables the optional parallel translation to be used as a macro for systems of optional parallelism to be model-checked with existing model-checkers. Optional parallelism has been studied in depth in the traces domain of CSP and the work of this dissertation shows that optional parallelism can be applied in the field of WSNs, as well as to define systems with optional parallel behaviour by using classical CSP operators. It is therefore a new construct which can be used with existing operational semantics of the operators of CSP