Development of real-time process control systems using formal techniques

A major application of computers has been to control physical processes in which the computer is embedded within some large physical process and is required to control concurrent physical processes. The main difficulty with these systems is their event-driven characteristics, which complicate their modelling and analysis. Although a number of researchers in the process system community have approached the problems of modelling and analysis of such systems, there is still a lack of standardised software development formalisms for the system (controller) development, particular at early stage of the system design cycle. This research forms part of a larger research programme which is concerned with the development of real-time process-control systems in which software is used to control concurrent physical processes. The general objective of the research in this thesis is to investigate the use of formal techniques in the analysis of such systems at their early stages of development, with a particular bias towards an application to high speed machinery. Specifically, the research aims to generate a standardised software development formalism for real-time process-control systems, particularly for software controller synthesis. In this research, a graphical modelling formalism called Sequential Function Chart (SFC), a variant of Grafcet, is examined. SFC, which is defined in the international standard IEC1131 as a graphical description language, has been used widely in industry and has achieved an acceptable level of maturity and acceptance. A comparative study between SFC and Petri nets is presented in this thesis. To overcome identified inaccuracies in the SFC, a formal definition of the firing rules for SFC is given. To provide a framework in which SFC models can be analysed formally, an extended time-related Petri net model for SFC is proposed and the transformation method is defined. The SFC notation lacks a systematic way of synthesising system models from the real world systems. Thus a standardised approach to the development of real-time process control systems is required such that the system (software) functional requirements can be identified, captured, analysed. A rule-based approach and a method called system behaviour driven method (SBDM) are proposed as a development formalism for real-time process-control systems.

Real-time intensity domain characterization of fibre lasers using spatio-temporal dynamics

Fibre lasers are light sources that are synonymous with stability. They can give rise to highly coherent continuous-wave radiation, or a stable train of mode locked pulses with well-defined characteristics. However, they can also exhibit an exceedingly diverse range of nonlinear operational regimes spanning a multi-dimensional parameter space. The complex nature of the dynamics poses significant challenges in the theoretical and experimental studies of such systems. Here, we demonstrate how the real-time experimental methodology of spatio-temporal dynamics can be used to unambiguously identify and discern between such highly complex lasing regimes. This two-dimensional representation of laser intensity allows the identification and tracking of individual features embedded in the radiation as they make round-trip circulations inside the cavity. The salient features of this methodology are highlighted by its application to the case of Raman fibre lasers and a partially mode locked ring fibre laser operating in the normal dispersion regime.