Pragmatic approach to the development of robust real-time protocols

This research is concerned with the development of distributed real-time systems, in which software is used for the control of concurrent physical processes. These distributed control systems are required to periodically coordinate the operation of several autonomous physical processes, with the property of an atomic action. The implementation of this coordination must be fault-tolerant if the integrity of the system is to be maintained in the presence of processor or communication failures. Commit protocols have been widely used to provide this type of atomicity and ensure consistency in distributed computer systems. The objective of this research is the development of a class of robust commit protocols, applicable to the coordination of distributed real-time control systems. Extended forms of the standard two phase commit protocol, that provides fault-tolerant and real-time behaviour, were developed. Petri nets are used for the design of the distributed controllers, and to embed the commit protocol models within these controller designs. This composition of controller and protocol model allows the analysis of the complete system in a unified manner. A common problem for Petri net based techniques is that of state space explosion, a modular approach to both the design and analysis would help cope with this problem. Although extensions to Petri nets that allow module construction exist, generally the modularisation is restricted to the specification, and analysis must be performed on the (flat) detailed net. The Petri net designs for the type of distributed systems considered in this research are both large and complex. The top down, bottom up and hybrid synthesis techniques that are used to model large systems in Petri nets are considered. A hybrid approach to Petri net design for a restricted class of communicating processes is developed. Designs produced using this hybrid approach are modular and allow re-use of verified modules. In order to use this form of modular analysis, it is necessary to project an equivalent but reduced behaviour on the modules used. These projections conceal events local to modules that are not essential for the purpose of analysis. To generate the external behaviour, each firing sequence of the subnet is replaced by an atomic transition internal to the module, and the firing of these transitions transforms the input and output markings of the module. Thus local events are concealed through the projection of the external behaviour of modules. This hybrid design approach preserves properties of interest, such as boundedness and liveness, while the systematic concealment of local events allows the management of state space. The approach presented in this research is particularly suited to distributed systems, as the underlying communication model is used as the basis for the interconnection of modules in the design procedure. This hybrid approach is applied to Petri net based design and analysis of distributed controllers for two industrial applications that incorporate the robust, real-time commit protocols developed. Temporal Petri nets, which combine Petri nets and temporal logic, are used to capture and verify causal and temporal aspects of the designs in a unified manner.

A methodology for analysis and control of discrete event dynamic systems

The rapid developments in computer technology have resulted in a widespread use of discrete event dynamic systems (DEDSs). This type of system is complex because it exhibits properties such as concurrency, conflict and non-determinism. It is therefore important to model and analyse such systems before implementation to ensure safe, deadlock free and optimal operation. This thesis investigates current modelling techniques and describes Petri net theory in more detail. It reviews top down, bottom up and hybrid Petri net synthesis techniques that are used to model large systems and introduces on object oriented methodology to enable modelling of larger and more complex systems. Designs obtained by this methodology are modular, easy to understand and allow re-use of designs. Control is the next logical step in the design process. This thesis reviews recent developments in control DEDSs and investigates the use of Petri nets in the design of supervisory controllers. The scheduling of exclusive use of resources is investigated and an efficient Petri net based scheduling algorithm is designed and a re-configurable controller is proposed. To enable the analysis and control of large and complex DEDSs, an object oriented C++ software tool kit was developed and used to implement a Petri net analysis tool, Petri net scheduling and control algorithms. Finally, the methodology was applied to two industrial DEDSs: a prototype can sorting machine developed by Eurotherm Controls Ltd., and a semiconductor testing plant belonging to SGS Thomson Microelectronics Ltd.

The design of robust protocols for distributed real-time systems

Modern distributed control systems comprise of a set of processors which are interconnected using a suitable communication network. For use in real-time control environments, such systems must be deterministic and generate specified responses within critical timing constraints. Also, they should be sufficiently robust to survive predictable events such as communication or processor faults. This thesis considers the problem of coordinating and synchronizing a distributed real-time control system under normal and abnormal conditions. Distributed control systems need to periodically coordinate the actions of several autonomous sites. Often the type of coordination required is the all or nothing property of an atomic action. Atomic commit protocols have been used to achieve this atomicity in distributed database systems which are not subject to deadlines. This thesis addresses the problem of applying time constraints to atomic commit protocols so that decisions can be made within a deadline. A modified protocol is proposed which is suitable for real-time applications. The thesis also addresses the problem of ensuring that atomicity is provided even if processor or communication failures occur. Previous work has considered the design of atomic commit protocols for use in non time critical distributed database systems. However, in a distributed real-time control system a fault must not allow stringent timing constraints to be violated. This thesis proposes commit protocols using synchronous communications which can be made resilient to a single processor or communication failure and still satisfy deadlines. Previous formal models used to design commit protocols have had adequate state coverability but have omitted timing properties. They also assumed that sites communicated asynchronously and omitted the communications from the model. Timed Petri nets are used in this thesis to specify and design the proposed protocols which are analysed for consistency and timeliness. Also the communication system is mcxielled within the Petri net specifications so that communication failures can be included in the analysis. Analysis of the Timed Petri net and the associated reachability tree is used to show the proposed protocols always terminate consistently and satisfy timing constraints. Finally the applications of this work are described. Two different types of applications are considered, real-time databases and real-time control systems. It is shown that it may be advantageous to use synchronous communications in distributed database systems, especially if predictable response times are required. Emphasis is given to the application of the developed commit protocols to real-time control systems. Using the same analysis techniques as those used for the design of the protocols it can be shown that the overall system performs as expected both functionally and temporally.

The development of hard real-time systems using a formal approach

Hard real-time systems are a class of computer control systems that must react to demands of their environment by providing `correct' and timely responses. Since these systems are increasingly being used in systems with safety implications, it is crucial that they are designed and developed to operate in a correct manner. This thesis is concerned with developing formal techniques that allow the specification, verification and design of hard real-time systems. Formal techniques for hard real-time systems must be capable of capturing the system's functional and performance requirements, and previous work has proposed a number of techniques which range from the mathematically intensive to those with some mathematical content. This thesis develops formal techniques that contain both an informal and a formal component because it is considered that the informality provides ease of understanding and the formality allows precise specification and verification. Specifically, the combination of Petri nets and temporal logic is considered for the specification and verification of hard real-time systems. Approaches that combine Petri nets and temporal logic by allowing a consistent translation between each formalism are examined. Previously, such techniques have been applied to the formal analysis of concurrent systems. This thesis adapts these techniques for use in the modelling, design and formal analysis of hard real-time systems. The techniques are applied to the problem of specifying a controller for a high-speed manufacturing system. It is shown that they can be used to prove liveness and safety properties, including qualitative aspects of system performance. The problem of verifying quantitative real-time properties is addressed by developing a further technique which combines the formalisms of timed Petri nets and real-time temporal logic. A unifying feature of these techniques is the common temporal description of the Petri net. A common problem with Petri net based techniques is the complexity problems associated with generating the reachability graph. This thesis addresses this problem by using concurrency sets to generate a partial reachability graph pertaining to a particular state. These sets also allows each state to be checked for the presence of inconsistencies and hazards. The problem of designing a controller for the high-speed manufacturing system is also considered. The approach adopted mvolves the use of a model-based controller: This type of controller uses the Petri net models developed, thus preservIng the properties already proven of the controller. It. also contains a model of the physical system which is synchronised to the real application to provide timely responses. The various way of forming the synchronization between these processes is considered and the resulting nets are analysed using concurrency sets.

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.

A design environment for deadlock-free concurrent software

Using current software engineering technology, the robustness required for safety critical software is not assurable. However, different approaches are possible which can help to assure software robustness to some extent. For achieving high reliability software, methods should be adopted which avoid introducing faults (fault avoidance); then testing should be carried out to identify any faults which persist (error removal). Finally, techniques should be used which allow any undetected faults to be tolerated (fault tolerance). The verification of correctness in system design specification and performance analysis of the model, are the basic issues in concurrent systems. In this context, modeling distributed concurrent software is one of the most important activities in the software life cycle, and communication analysis is a primary consideration to achieve reliability and safety. By and large fault avoidance requires human analysis which is error prone; by reducing human involvement in the tedious aspect of modelling and analysis of the software it is hoped that fewer faults will persist into its implementation in the real-time environment. The Occam language supports concurrent programming and is a language where interprocess interaction takes place by communications. This may lead to deadlock due to communication failure. Proper systematic methods must be adopted in the design of concurrent software for distributed computing systems if the communication structure is to be free of pathologies, such as deadlock. The objective of this thesis is to provide a design environment which ensures that processes are free from deadlock. A software tool was designed and used to facilitate the production of fault-tolerant software for distributed concurrent systems. Where Occam is used as a design language then state space methods, such as Petri-nets, can be used in analysis and simulation to determine the dynamic behaviour of the software, and to identify structures which may be prone to deadlock so that they may be eliminated from the design before the program is ever run. This design software tool consists of two parts. One takes an input program and translates it into a mathematical model (Petri-net), which is used for modeling and analysis of the concurrent software. The second part is the Petri-net simulator that takes the translated program as its input and starts simulation to generate the reachability tree. The tree identifies `deadlock potential' which the user can explore further. Finally, the software tool has been applied to a number of Occam programs. Two examples were taken to show how the tool works in the early design phase for fault prevention before the program is ever run.

Computer control of machines utilising independent drive mechanisms

The thesis describes an investigation into methods for the specification, design and implementation of computer control systems for flexible manufacturing machines comprising multiple, independent, electromechanically-driven mechanisms. An analysis is made of the elements of conventional mechanically-coupled machines in order that the operational functions of these elements may be identified. This analysis is used to define the scope of requirements necessary to specify the format, function and operation of a flexible, independently driven mechanism machine. A discussion of how this type of machine can accommodate modern manufacturing needs of high-speed and flexibility is presented. A sequential method of capturing requirements for such machines is detailed based on a hierarchical partitioning of machine requirements from product to independent drive mechanism. A classification of mechanisms using notations, including Data flow diagrams and Petri-nets, is described which supports capture and allows validation of requirements. A generic design for a modular, IDM machine controller is derived based upon hierarchy of control identified in these machines. A two mechanism experimental machine is detailed which is used to demonstrate the application of the specification, design and implementation techniques. A computer controller prototype and a fully flexible implementation for the IDM machine, based on Petri-net models described using the concurrent programming language Occam, is detailed. The ability of this modular computer controller to support flexible, safe and fault-tolerant operation of the two intermittent motion, discrete-synchronisation independent drive mechanisms is presented. The application of the machine development methodology to industrial projects is established.

The design of fault tolerant software for loosely coupled distributed systems

Requirements for systems to continue to operate satisfactorily in the presence of faults has led to the development of techniques for the construction of fault tolerant software. This thesis addresses the problem of error detection and recovery in distributed systems which consist of a set of communicating sequential processes. A method is presented for the `a priori' design of conversations for this class of distributed system. Petri nets are used to represent the state and to solve state reachability problems for concurrent systems. The dynamic behaviour of the system can be characterised by a state-change table derived from the state reachability tree. Systematic conversation generation is possible by defining a closed boundary on any branch of the state-change table. By relating the state-change table to process attributes it ensures all necessary processes are included in the conversation. The method also ensures properly nested conversations. An implementation of the conversation scheme using the concurrent language occam is proposed. The structure of the conversation is defined using the special features of occam. The proposed implementation gives a structure which is independent of the application and is independent of the number of processes involved. Finally, the integrity of inter-process communications is investigated. The basic communication primitives used in message passing systems are seen to have deficiencies when applied to systems with safety implications. Using a Petri net model a boundary for a time-out mechanism is proposed which will increase the integrity of a system which involves inter-process communications.

Effects of several coloured interventions on reading performance in age-related macular degeneration (ARMD)

A literature review revealed that very little work has been conducted to investigate the possible benefits of coloured interventions on reading performance in low vision due to ARMD, under conditions that are similar to the real world reading environment. Further studies on the use of colour, as a rehabilitative intervention in low vision would therefore be useful. A series of objective, subject based, age-similar controlled experiments were used to address the primary aims. Trends in some of the ARMD data suggested better reading performance with blue or green illuminance but there were also some individuals who performed better with yellow, or with illuminance of reduced intensity. Statistically, better reading in general occurred with a specialised yellow photochromic lens and also a clear lens than with a fixed lens or a neutral density filter. No reading advantage was gained from using the coloured screen facility of a video-magnifier. Some subjects with low vision were found to have co-existent binocular vision anomalies, which may have caused reading difficulties similar to those produced by ARMD. Some individuals with ARMD benefited from the use of increased local illuminance produced by either a standard tungsten or compact fluorescent lamp. No reading improvement occurred with a daylight simulation tungsten lamp. The Intuitive Colorimeter® can be used to detect and map out colour vision discrimination deficiency in ARMD and the Humphrey 630 Visual Field Analyser can be used to analyse the biocular visual field in subjects with ARMD. Some experiments highlighted a positive effect of a blue intervention in reading with ARMD.

Functional and perceived benefits of wearing coloured filters by patients with age-related macular degeneration

Background: The aim was to investigate the visual effect of coloured filters compared to transmission-matched neutral density filters, in patients with dry age-related macular degeneration. Methods: Visual acuity (VA, logMAR), contrast sensitivity (Pelli-Robson) and colour vision (D15) were recorded for 39 patients (average age 79.1 ± 7.2 years) with age-related macular degeneration, both in the presence and absence of glare from a fluorescent source. Patients then chose their preferred coloured and matched neutral density transmission filters (NoIR). Visual function tests were repeated with the chosen filters, both in the presence and absence of glare from the fluorescent source. Patients trialled the two filters for two weeks each, in random order. Following the trial of each filter, a telephone questionnaire was completed. Results: VA and contrast sensitivity were unaffected by the coloured filters but reduced through the neutral density filters (p < 0.01). VA and contrast sensitivity were reduced by similar amounts, following the introduction of the glare source, both in the presence and absence of filters (p < 0.001). Colour vision error scores were increased following the introduction of a neutral density filter (from 177.6 ± 60.2 to 251.9 ± 115.2) and still further through coloured filters (275.1 ± 50.8; p < 0.001). In the absence of any filter, colour vision error scores increased by 29.1 ± 55.60 units in the presence of glare (F2,107 = 3.9, p = 0.02); however, there was little change in colour vision error scores, in the presence of glare, with either the neutral density or coloured filters. Questionnaires indicated that patients tended to gain more benefit from the coloured filters. Conclusions: Coloured filters had minimal impact on VA and contrast sensitivity in patients with age-related macular degeneration; however, they caused a small reduction in objective colour vision, although this was not registered subjectively by patients. Patients indicated that they received more benefit from the coloured filters compared with neutral density filters. © 2013 The Authors © 2013 Optometrists Association Australia.

Belief nets for mental health

DUE TO COPYRIGHT RESTRICTIONS ONLY AVAILABLE FOR CONSULTATION AT ASTON UNIVERSITY LIBRARY AND INFORMATION SERVICES WITH PRIOR ARRANGEMENT

The effects of coloured light filter overlays on reading rates in age-related macular degeneration

Purpose: To determine the effect of coloured light filter overlays on reading rates for people with age-related macular degeneration (AMD). Method: Using a prospective clinical trial design, we examined the null hypothesis that coloured light filter overlays do not improve reading rates in AMD when compared to a clear filter. Reading rates for 12 subjects with non-exudative AMD, associated with a relative scotoma and central fixation (mean age 81 years, SD 5.07 years) were determined using the Rate of Reading Test® (printed, nonsense, lower case sans serif, stationary text) with 10 different, coloured light filter overlays (Intuitive Overlays®; figures in brackets are percentage transmission values); rose (78%), pink (78%), purple (67%), aqua (81%), blue (74%), lime-green (86%), mint-green (85%), yellow (93%), orange (83%) and grey (71%). A clear overlay (Roscolene # 00) (360 cdm-2) with 100% transmittance was used as a control. Results: ANOVA indicated that there was no statistically significant difference in reading rates with the coloured light filter overlays compared to the clear filter. Furthermore, chi-squared analysis indicated that the rose, purple and blue filters had a significantly poorer overall ranking in terms of reading rates compared to the other coloured and clear light filters. Conclusion: Coloured light filter overlays are unlikely to provide a clinically significant improvement in reading rates for people with non-exudative AMD associated with a relative scotoma and central fixation. Copyright © Acta Ophthalmol Scand 2004.

Pupil responses associated with coloured afterimages are mediated by the magno-cellular pathway

Sustained fixation of a bright coloured stimulus will, on extinction of the stimulus and continued steady fixation, induce an afterimage whose colour is complementary to that of the initial stimulus; an effect thought to be caused by fatigue of cones and/or of cone-opponent processes to different colours. However, to date, very little is known about the specific pathway that causes the coloured afterimage. Using isoluminant coloured stimuli recent studies have shown that pupil constriction is induced by onset and offset of the stimulus, the latter being attributed specifically to the subsequent emergence of the coloured afterimage. The aim of the study was to investigate how the offset pupillary constriction is generated in terms of input signals from discrete functional elements of the magno- and/or parvo-cellular pathways, which are known principally to convey, respectively, luminance and colour signals. Changes in pupil size were monitored continuously by digital analysis of an infra-red image of the pupil while observers viewed isoluminant green pulsed, ramped or luminance masked stimuli presented on a computer monitor. It was found that the amplitude of the offset pupillary constriction decreases when a pulsed stimulus is replaced by a temporally ramped stimulus and is eliminated by a luminance mask. These findings indicate for the first time that pupillary constriction associated with a coloured afterimage is mediated by the magno-cellular pathway. © 2003 Elsevier Science Ltd. All rights reserved.

Benefit of coloured lenses for age-related macular degeneration

Purpose: To evaluate and compare the functional and perceived benefits of wearing coloured lenses by patients with age-related macular degeneration (ARMD). Method: Ten subjects with early ARMD and five elderly controls wore a selection of NoIR wrap-around coloured lenses (yellow 29.7% light transmission, orange 22.9%, red 16.8% and grey 10.3%), each for a duration of 7 days. Contrast sensitivity, colour vision, visual acuity, the effect of glare and peripheral sensitivity were measured for each lens and compared with a control (no lens) condition. Subjective ratings of visual performance were also scored. Results: Compared with the no filter condition, red and grey lenses reduced contrast sensitivity whereas yellow and orange lenses increased contrast sensitivity. These objective changes were supported by subjective ratings in subjects with ARMD. Grey lenses reduced the loss of contrast sensitivity usually suffered in the presence of glare, whereas visual acuity and peripheral sensitivity decreased with red lenses. Colour vision became distorted with red lenses in control subjects, but was relatively unaffected by the use of coloured lenses in subjects with ARMD. Conclusions: The subjective benefit of coloured lenses appears to be due to a minor enhancement of contrast sensitivity. © 2002 The College of Optometrists.