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
Dissertation (MEng) -- University of Pretoria 2015.