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.

Altered resting-state EEG source functional connectivity in schizophrenia:the effect of illness duration

Despite the increasing body of evidence supporting the hypothesis of schizophrenia as a disconnection syndrome, studies of resting-state EEG Source Functional Connectivity (EEG-SFC) in people affected by schizophrenia are sparse. The aim of the present study was to investigate resting-state EEG-SFC in 77 stable, medicated patients with schizophrenia (SCZ) compared to 78 healthy volunteers (HV). In order to study the effect of illness duration, SCZ were divided in those with a short duration of disease (SDD; n = 25) and those with a long duration of disease (LDD; n = 52). Resting-state EEG recordings in eyes closed condition were analyzed and lagged phase synchronization (LPS) indices were calculated for each ROI pair in the source-space EEG data. In delta and theta bands, SCZ had greater EEG-SFC than HV; a higher theta band connectivity in frontal regions was observed in LDD compared with SDD. In the alpha band, SCZ showed lower frontal EEG-SFC compared with HV whereas no differences were found between LDD and SDD. In the beta1 band, SCZ had greater EEG-SFC compared with HVs and in the beta2 band, LDD presented lower frontal and parieto-temporal EEG-SFC compared with HV. In the gamma band, SDD had greater connectivity values compared with LDD and HV. This study suggests that resting state brain network connectivity is abnormally organized in schizophrenia, with different patterns for the different EEG frequency components and that EEG can be a powerful tool to further elucidate the complexity of such disordered connectivity.