Verification of floating point programs

In this thesis we present an approach to automated verification of floating point programs. Existing techniques for automated generation of correctness theorems are extended to produce proof obligations for accuracy guarantees and absence of floating point exceptions. A prototype automated real number theorem prover is presented, demonstrating a novel application of function interval arithmetic in the context of subdivision-based numerical theorem proving. The prototype is tested on correctness theorems for two simple yet nontrivial programs, proving exception freedom and tight accuracy guarantees automatically. The prover demonstrates a novel application of function interval arithmetic in the context of subdivision-based numerical theorem proving. The experiments show how function intervals can be used to combat the information loss problems that limit the applicability of traditional interval arithmetic in the context of hard real number theorem proving.

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.

The effect of age, gender and driver status on pedestrians' intentions to cross the road in risky situations

The theory of planned behaviour (TPB) has been used successfully in the past to account for pedestrians' intentions to cross the road in risky situations. However, accident statistics show age and gender differences in the likelihood of adult pedestrian accidents. This study extends earlier work by examining the relative importance of the model components as predictors of intention to cross for four different adult age groups, men, women, drivers and nondrivers. The groups did not differ in the extent to which they differentiated between two situations of varying perceived risk. The model fit was good, but accounted for less of the variance in intention for the youngest group (17-24) than for other age groups. Differences between the age groups in intention to cross seemed to be due to differences in perceived value of crossing rather than differences in perceived risk. Women were less likely to intend to cross than men and perceived more risk, and there were important age, gender and driver status differences in the importance of the TPB variables as predictors of intention. A key implication of these findings is that road safety interventions need to be designed differently for different groups. © 2006 Elsevier Ltd. All rights reserved.

Verification of the standard model of the photorefractive nonlinearity in BSO crystals

On the basis of the standard model for the photorefractive nonlinearity we investigate whether a systematic description of the dependence of two-beam energy exchange on beam polarization and grating vector K is possible. Our result is that there is good agreement between theory and experiment with respect to the polarization properties and semi-quantitative agreement with respect to the K-dependence of the energy exchange.

Verification and validation of numerical models of the transport of insulation debris

Damage to insulation materials located near to a primary circuit coolant leak may compromise the operation of the emergency core cooling system (ECCS). Insulation material in the form of mineral wool fiber agglomerates (MWFA) maybe transported to the containment sump strainers, where they may block or penetrate the strainers. Though the impact of MWFA on the pressure drop across the strainers is minimal, corrosion products formed over time may also accumulate in the fiber cakes on the strainers, which can lead to a significant increase in the strainer pressure drop and result in cavitation in the ECCS. An experimental and theoretical study performed by the Helmholtz-Zentrum Dresden-Rossendorf and the Hochschule Zittau/Görlitz is investigating the phenomena that maybe observed in the containment vessel during a primary circuit coolant leak. The study entails the generation of fiber agglomerates, the determination of their transport properties in single and multi-effect experiments and the long-term effect that corrosion and erosion of the containment internals by the coolant has on the strainer pressure drop. The focus of this paper is on the verification and validation of numerical models that can predict the transport of MWFA. A number of pseudo-continuous dispersed phases of spherical wetted agglomerates represent the MWFA. The size, density, the relative viscosity of the fluid-fiber agglomerate mixture and the turbulent dispersion all affect how the fiber agglomerates are transported. In the cases described here, the size is kept constant while the density is modified. This definition affects both the terminal velocity and volume fraction of the dispersed phases. Note that the relative viscosity is only significant at high concentrations. Three single effect experiments were used to provide validation data on the transport of the fiber agglomerates under conditions of sedimentation in quiescent fluid, sedimentation in a horizontal flow and suspension in a horizontal flow. The experiments were performed in a rectangular column for the quiescent fluid and a racetrack type channel that provided a near uniform horizontal flow. The numerical models of sedimentation in the column and the racetrack channel found that the sedimentation characteristics are consistent with the experiments. For channel suspension, the heavier fibers tend to accumulate at the channel base even at high velocities, while lighter phases are more likely to be transported around the channel.

Modelling and experimental verification of a solar-powered liquid desiccant cooling system for greenhouse food production in hot climates

Experiments and theoretical modelling have been carried out to predict the performance of a solar-powered liquid desiccant cooling system for greenhouses. We have tested two components of the system in the laboratory using MgCl2 desiccant: (i) a regenerator which was tested under a solar simulator and (ii) a desiccator which was installed in a test duct. Theoretical models have been developed for both regenerator and desiccator and gave good agreement with the experiments. The verified computer model is used to predict the performance of the whole system during the hot summer months in Mumbai, Chittagong, Muscat, Messina and Havana. Taking examples of temperate, sub-tropical, tropical and heat-tolerant tropical crops (lettuce, soya bean, tomato and cucumber respectively) we estimate the extensions in growing seasons enabled by the system. Compared to conventional evaporative cooling, the desiccant system lowers average daily maximum temperatures in the hot season by 5.5-7.5 °C, sufficient to maintain viable growing conditions for lettuce throughout the year. In the case of tomato, cucumber and soya bean the system enables optimal cultivation through most summer months. It is concluded that the concept is technically viable and deserves testing by means of a pilot installation at an appropriate location.

Influence of personal mobile phone ringing and usual intention to answer on driver error

Given evidence of effects of mobile phone use on driving, and also legislation, many careful drivers refrain from answering their phones when driving. However, the distracting influence of a call on driving, even in the context of not answering, has not been examined. Furthermore, given that not answering may be contrary to an individual’s normal habits, this study examined whether distraction caused by the ignored call varies according to normal intention to answer whilst driving. That is, determining whether the effect is more than a simple matter of noise distraction. Participants were 27 young drivers (18-29 years), all regular mobile users. A Theory of Planned Behaviour questionnaire examined predictors of intention to refrain from answering calls whilst driving. Participants provided their mobile phone number and were instructed not to answer their phone if it were to ring during a driving simulation. The simulation scenario had seven hazards (e.g. car pulling out, pedestrian crossing) with three being immediately preceded by a call. Infractions (e.g. pedestrian collisions, vehicle collisions, speed exceedances) were significantly greater when distracted by call tones than with no distraction. Lower intention to ignore calls whilst driving correlated with a larger effect of distraction, as was feeling unable to control whether one answered whilst driving (Perceived Behavioural Control). The study suggests that even an ignored call can cause significantly increased infractions in simulator driving, with pedestrian collisions and speed exceedances being striking examples. Results are discussed in relation to cognitive demands of inhibiting normal behaviour and to drivers being advised to switch phones off whilst driving.

Experimental verification of the dispersion tolerance improvement of partial DPSK with optimised filtering

We experimentally confirm the optimum combination of modulator delay and filter bandwidth to maximize the dispersion tolerance of partial DPSK.

Opportunity, fair process and relationship value:career development as a driver of proactive work behaviour

In line with recent findings from organisational justice theory, we hypothesised that employee proactive behaviour and careerist orientation is predicted by the interplay of perceived favourability of career development opportunities, the perceived fairness of the procedures used to decide them, and employee organisational commitment. Employees (N = 325) of a large financial services organisation responded to a self-completion questionnaire. As predicted, when career development opportunities were viewed unfavourably, perceived procedural justice was significantly and positively related to individual proactive behaviour and significantly and negatively related to careerist orientation but only when organisational commitment was high. It appears that high procedural justice may only 'offset' the negative effects of unfavourable career development opportunities when employees identify with, and are committed to, their organisation. Further support is presented for a relational, rather than instrumental, model of procedural justice when reflecting on employee reactions to their employers' policies and decision-making. Implications for theory and practice are discussed.

Charismatic leadership as a driver of sales-marketing collaboration

The purpose of this study is to develop an integrative framework for investigating the organizational consequences of marketing leadership. The new integrative framework employs the theories of charismatic leadership and organizational identification as foundation. Combining constructs and propositions from these two theories, and informed by initial insights from in-depth interview research, our proposed framework offers an holistic model to explore and explain how marketing leadership behaviours influence (1) relations between marketing and sales groups, and (2) consequent firm performance. The paper develops propositions and offers future research directions.

Validation and verification of embedded neural systems

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

Validation and verification of embedded neural systems

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

Verification of the standard model of the photorefractive nonlinearity in BSO crystals

On the basis of the standard model for the photorefractive nonlinearity we investigate whether a systematic description of the dependence of two-beam energy exchange on beam polarization and grating vector K is possible. Our result is that there is good agreement between theory and experiment with respect to the polarization properties and semi-quantitative agreement with respect to the K-dependence of the energy exchange.

Experimental verification of four wave mixing efficiency characteristics in a few mode fibre

We introduce two techniques to measure the efficiency of inter mode FWM with respect to intra mode FWM. The first technique allows an estimation of the additional FWM penalty for any given system; the second isolates the contribution of each mode. Measurements are compared to an analytical model showing the FWM signal increases by ∼2dB with inter mode phase matching.