A formal methodology for the verification of concurrent systems

There is an increasing emphasis on the use of software to control safety critical plants for a wide area of applications. The importance of ensuring the correct operation of such potentially hazardous systems points to an emphasis on the verification of the system relative to a suitably secure specification. However, the process of verification is often made more complex by the concurrency and real-time considerations which are inherent in many applications. A response to this is the use of formal methods for the specification and verification of safety critical control systems. These provide a mathematical representation of a system which permits reasoning about its properties. This thesis investigates the use of the formal method Communicating Sequential Processes (CSP) for the verification of a safety critical control application. CSP is a discrete event based process algebra which has a compositional axiomatic semantics that supports verification by formal proof. The application is an industrial case study which concerns the concurrent control of a real-time high speed mechanism. It is seen from the case study that the axiomatic verification method employed is complex. It requires the user to have a relatively comprehensive understanding of the nature of the proof system and the application. By making a series of observations the thesis notes that CSP possesses the scope to support a more procedural approach to verification in the form of testing. This thesis investigates the technique of testing and proposes the method of Ideal Test Sets. By exploiting the underlying structure of the CSP semantic model it is shown that for certain processes and specifications the obligation of verification can be reduced to that of testing the specification over a finite subset of the behaviours of the process.

Factors affecting corneoscleral topography

PURPOSE: To evaluate factors affecting corneoscleral profile (CSP) using Anterior Segment Optical Coherence Tomography (AS-OCT) in combination with conventional videokeratoscopy. METHODS: OCT data were collected from 204 subjects of mean age 34.9 years (SD: ±15.2 yrs, range 18 to 65) using the Zeiss Visante AS-OCT and Medmont M300 corneal topographer. Measurements of corneal diameter (CD), corneal sagittal height (CS), iris diameter (ID), corneoscleral junction angle (CSJ) and scleral radius (SR) were extracted from multiple OCT images. Horizontal visible iris diameter (HVID) and vertical palpebral aperture (PA) were measured using a slit lamp graticule. Subject body height was also measured. Associations were then sought between CSP variables and age, height, ethnicity, sex and refractive error data collected. Results: Significant correlations were found between age and ocular topography variables of HVID, PA, CSJ, SR and ID (P<0.0001), while height correlated with HVID, CD and ID, and power vector terms only with vertical plane keratometry, CD and CS. Significant differences were noted between ethnicities with respect to CD (P=0.0046), horizontal and vertical CS (P=0.0068 and P=0.0095), and also horizontal ID (P=0.0010), while the same variables, with the exception of vertical CS, also varied with sex; horizontal CD (P=0.0018), horizontal CS (P=0.0018) and ID (P=0.0012). Age accounted for up to 36% of the variance in CSP variables. Conclusion: Age is the main factor influencing corneoscleral topography; consequently, this should be taken into consideration in contact lens design, in the optimization of surgical procedures involving the cornea and sclera and in IOL selection.

Determining the number of nodes for wireless sensor networks

The number of nodes has large impact on the performance, lifetime and cost of wireless sensor network (WSN). It is difficult to determine, because it depends on many factors, such as the network protocols, the collaborative signal processing (CSP) algorithms, etc. A mathematical model is proposed in this paper to calculate the number based on the required working time. It can be used in the general situation by treating these factors as the parameters of energy consumption. © 2004 IEEE.

Use of imaging technology to better understand soft contact lens fit dynamics

The principal theme of this thesis is the identification of additional factors affecting, and consequently to better allow, the prediction of soft contact lens fit. Various models have been put forward in an attempt to predict the parameters that influence soft contact lens fit dynamics; however, the factors that influence variation in soft lens fit are still not fully understood. The investigations in this body of work involved the use of a variety of different imaging techniques to both quantify the anterior ocular topography and assess lens fit. The use of Anterior-Segment Optical Coherence Tomography (AS-OCT) allowed for a more complete characterisation of the cornea and corneoscleral profile (CSP) than either conventional keratometry or videokeratoscopy alone, and for the collection of normative data relating to the CSP for a substantial sample size. The scleral face was identified as being rotationally asymmetric, the mean corneoscleral junction (CSJ) angle being sharpest nasally and becoming progressively flatter at the temporal, inferior and superior limbal junctions. Additionally, 77% of all CSJ angles were within ±50 of 1800, demonstrating an almost tangential extension of the cornea to form the paralimbal sclera. Use of AS-OCT allowed for a more robust determination of corneal diameter than that of white-to-white (WTW) measurement, which is highly variable and dependent on changes in peripheral corneal transparency. Significant differences in ocular topography were found between different ethnicities and sexes, most notably for corneal diameter and corneal sagittal height variables. Lens tightness was found to be significantly correlated with the difference between horizontal CSJ angles (r =+0.40, P =0.0086). Modelling of the CSP data gained allowed for prediction of up to 24% of the variance in contact lens fit; however, it was likely that stronger associations and an increase in the modelled prediction of variance in fit may have occurred had an objective method of lens fit assessment have been made. A subsequent investigation to determine the validity and repeatability of objective contact lens fit assessment using digital video capture showed no significant benefit over subjective evaluation. The technique, however, was employed in the ensuing investigation to show significant changes in lens fit between 8 hours (the longest duration of wear previously examined) and 16 hours, demonstrating that wearing time is an additional factor driving lens fit dynamics. The modelling of data from enhanced videokeratoscopy composite maps alone allowed for up to 77% of the variance in soft contact lens fit, and up to almost 90% to be predicted when used in conjunction with OCT. The investigations provided further insight into the ocular topography and factors affecting soft contact lens fit.