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.

Cryptographic techniques for personal communication systems security

The advent of personal communication systems within the last decade has depended upon the utilization of advanced digital schemes for source and channel coding and for modulation. The inherent digital nature of the communications processing has allowed the convenient incorporation of cryptographic techniques to implement security in these communications systems. There are various security requirements, of both the service provider and the mobile subscriber, which may be provided for in a personal communications system. Such security provisions include the privacy of user data, the authentication of communicating parties, the provision for data integrity, and the provision for both location confidentiality and party anonymity. This thesis is concerned with an investigation of the private-key and public-key cryptographic techniques pertinent to the security requirements of personal communication systems and an analysis of the security provisions of Second-Generation personal communication systems is presented. Particular attention has been paid to the properties of the cryptographic protocols which have been employed in current Second-Generation systems. It has been found that certain security-related protocols implemented in the Second-Generation systems have specific weaknesses. A theoretical evaluation of these protocols has been performed using formal analysis techniques and certain assumptions made during the development of the systems are shown to contribute to the security weaknesses. Various attack scenarios which exploit these protocol weaknesses are presented. The Fiat-Sharmir zero-knowledge cryptosystem is presented as an example of how asymmetric algorithm cryptography may be employed as part of an improved security solution. Various modifications to this cryptosystem have been evaluated and their critical parameters are shown to be capable of being optimized to suit a particular applications. The implementation of such a system using current smart card technology has been evaluated.

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.

An investigation into formal and functional characteristics of qualifications in legislative writing and its application to English for academic legal purposes.

The present investigation is based on a linguistic analysis of the 'Housing Act 1980' and attempts to examine the role of qualifications in the structuring of the legislative statement. The introductory chapter isolates legislative writing as a "sub-variety “of legal language and provides an overview of the controversies surrounding the way it is written and the problems it poses to its readers. Chapter two emphasizes the limitations of the available work on the description of language-varieties for the analysis of legislative writing and outlines the approach adopted for the present analysis. This chapter also gives some idea of the information-structuring of legislative provisions and establishes qualification as a key element in their textualisation. The next three chapters offer a detailed account of the ten major qualification-types identified in the corpus, concentrating on the surface form they take, the features of legislative statements they textualize and the syntactic positions to which they are generally assigned in the statement of legislative provisions. The emerging hypotheses in these chapters have often been verified through a specialist reaction from a Parliamentary Counsel, largely responsible for the writing of the ‘Housing Act 1980’• The findings suggest useful correlations between a number of qualificational initiators and the various aspects of the legislative statement. They also reveal that many of these qualifications typically occur in those clause-medial syntactic positions which are sparingly used in other specialist discourse, thus creating syntactic discontinuity in the legislative sentence. Such syntactic discontinuities, on the evidence from psycholinguistic experiments reported in chapter six, create special problems in the processing and comprehension of legislative statements. The final chapter converts the main linguistic findings into a series of pedagogical generalizations, offers indications of how this may be applied in EALP situations and concludes with other considerations of possible applications.

An applied linguistic analysis of the simplification of narrative texts

Simplification of texts has traditionally been carried out by replacing words and structures with appropriate semantic equivalents in the learner's interlanguage, omitting whichever items prove intractable, and thereby bringing the language of the original within the scope of the learner's transitional linguistic competence. This kind of simplification focuses mainly on the formal features of language. The simplifier can, on the other hand, concentrate on making explicit the propositional content and its presentation in the original in order to bring what is communicated in the original within the scope of the learner's transitional communicative competence. In this case, simplification focuses on the communicative function of the language. Up to now, however, approaches to the problem of simplification have been mainly concerned with the first kind, using the simplifier’s intuition as to what constitutes difficulty for the learner. There appear to be few objective principles underlying this process. The main aim of this study is to investigate the effect of simplification on the communicative aspects of narrative texts, which includes the manner in which narrative units at higher levels of organisation are structured and presented and also the temporal and logical relationships between lower level structures such as sentences/clauses, with the intention of establishing an objective approach to the problem of simplification based on a set of principled procedures which could be used as a guideline in the simplification of material for foreign students at an advanced level.

A sociological analysis of four police consultative committees in Birmingham

Consultation between the police and the community was a recommendation of Lord Scarman in his report into the Brixton riots in 1981. By 1982 the West Midlands Police Authority had established local consultative committees on each police sub-division. This thesis is a study of four Police Consultative Committees in Birmingham, using qualitative methods of attendance at committee meetings and interviews with committee members. The research was carried out between 1990 and 1992 - ten years after formal consultation was established, and aimed to examine the relationship between the micro social processes of the committees and key sociological theoretical concepts. The analysis of the four committees contextualises them within the social and political parameters of urban policing in the late 1980s. Each committee is taken as a case study to highlight the following aspects of consultation:- relations between the police and black communities; membership, representation and accountability; responding to community conflict; crime prevention agencies and networks of social control. The findings are then generalised to the sociological theoretical concepts of hegemony, legitimation, community conflict and social control. The central proposition of this thesis is that, whilst these committees are not fulfilling the role Lord Scarman envisaged for them (of involving local community representatives in policing strategies and policies), they do have important policing and political roles. It is argued that they offer a platform from which senior police officers can engage local people into supporting policing objectives without actually involving them in determining those objectives. Furthermore, such committees have political symbolism in that they enable the government to be seen to be responding to the issues of accountability and relations between the police and black communities following the urban disorders, without actually devolving any statutory powers to the community.

Minority enterprise in the clothing industry: an analysis of Asian jeans manufacturers in Birmingham

This thesis discusses and assesses the resources available to Asian entrepreneurs in the West Midlands' clothing industry and how they are used by these small businessmen in order to address opportunities in the market economy within the constraints imposed. The fashion industry is volatile and is dependent upon flexible firms which can respond quickly to shortrun production schedules. Small firms are best able to respond to this market environment. Production of jeans presents an interesting departure from the mainstream fashion industry. It is traditionally gared towards longrun production schedules where multinational enterprises have artificially diversified the market, promoting the 'right' brand name and have established control of the upper end of the market, whilst imports from Newly Developing Countries have catered for cheap copies at the lower end of the market. In recent years, a fashion element to jeans has emerged, thus opening a market gap for U.K. manufacturers to respond in the same way as for other fashion articles. A large immigrant population, previously serving the now declining factories and foundries of the West Midlands but, through redundancy, no longer a part of this employment sector, has ~5ponded to economic constraints and market opportunities by drawing on ethnic network resources for competitive access to labour, finance and contacts, to attack the emergent market gap. Two models of these Asian entrepreneurs are developed. One being somecne who has professionally and actively tackled the market gap and become established. These entrepreneurs are usually educated and have personal experience in business and were amongst the first to perceive opportunities to enter the industry, actively utilising their ethnicity as a resource upon which to draw for favorable access to cheap, flexible labour and capital. The second model is composed of later entrants to jeans manufacturing. They have less formal education and experience and have been pushed into self-employment by constraints of unemployment. Their ethnicity is passively used as a resource. They are more likely confined to the marginal activity of 'cut make and trim' and have little opportunity to increase profit margins, become estalished or expand.

On waveform analysis, the adaptive task technique, and the effect of vibration on manual control skill

A re-examination of fundamental concepts and a formal structuring of the waveform analysis problem is presented in Part I. eg. the nature of frequency is examined and a novel alternative to the classical methods of detection proposed and implemented which has the advantage of speed and independence from amplitude. Waveform analysis provides the link between Parts I and II. Part II is devoted to Human Factors and the Adaptive Task Technique. The Historical, Technical and Intellectual development of the technique is traced in a review which examines the evidence of its advantages relative to non-adaptive fixed task methods of training, skill assessment and man-machine optimisation. A second review examines research evidence on the effect of vibration on manual control ability. Findings are presented in terms of percentage increment or decrement in performance relative to performance without vibration in the range 0-0.6Rms'g'. Primary task performance was found to vary by as much as 90% between tasks at the same Rms'g'. Differences in task difficulty accounted for this difference. Within tasks vibration-added-difficulty accounted for the effects of vibration intensity. Secondary tasks were found to be largely insensitive to vibration except secondaries which involved fine manual adjustment of minor controls. Three experiments are reported next in which an adaptive technique was used to measure the % task difficulty added by vertical random and sinusoidal vibration to a 'Critical Compensatory Tracking task. At vibration intensities between 0 - 0.09 Rms 'g' it was found that random vibration added (24.5 x Rms'g')/7.4 x 100% to the difficulty of the control task. An equivalence relationship between Random and Sinusoidal vibration effects was established based upon added task difficulty. Waveform Analyses which were applied to the experimental data served to validate Phase Plane analysis and uncovered the development of a control and possibly a vibration isolation strategy. The submission ends with an appraisal of subjects mentioned in the thesis title.

The psychology of news influence and development of Media Framing Analysis

HowHow precisely do media influence their readers, listeners and viewers? In this paper, we argue that any serious study of the psychology of media influence must incorporate a systematic analysis of media material. However, psychology presently lacks a methodology for doing this that is sensitive to context, relying on generalised methods like content or discourse analysis. In this paper, we develop an argument to support our development of a technique that we have called Media Framing Analysis (MFA), a formal procedure for conducting analyses of (primarily news) media texts. MFA draws on elements of existing framing research from communication and other social scientific research while at the same time incorporating features of particular relevance to psychology, such as narrative and characterisation.

Information and behavioural instruction along the health-care pathway:the perspective of people undergoing hernia repair surgery and the role of formal and informal information sources

Provision of information and behavioural instruction has been demonstrated to improve recovery after surgery. However, patients draw on a range of information sources and it is important to establish which sources patients use and how this influences perceptions and behaviour as they progress along the surgical pathway. In this qualitative, exploratory and longitudinal study, the use of information and instruction were explored from the perspective of people undergoing inguinal hernia repair surgery. Seven participants undergoing inguinal hernia repair surgery were interviewed using semi-structured interviews 2 weeks before surgery and 2 weeks and 4 months post-surgery. Nineteen interviews were conducted in total. Topic guides included sources of knowledge, reasons for help-seeking and opting for surgery and factors influencing return to activity. Data were analysed thematically according to Interpretative Phenomenological Analysis. Participants sought information from a range of sources, focusing on informal information sources before surgery and using information and instruction from health-care professionals post-surgery. This information influenced behaviours including deciding to undergo surgery, use of pain medication and returning to usual activity. Anxiety and help-seeking resulted when unexpected post-surgical events occurred such as extensive bruising. Findings were consistent with psychological and sociological theories. Overall, participants were positive about the information and instruction they received but expressed a desire for more timely information on post-operative adverse events.

An exploratory analysis of corporate social responsibility:definitions, motives and values

Corporate Social Responsibility (CSR) is a multi-disciplinary subject and definitions vary with regard to the perceived scope or boundaries of the corporation’s responsibility. In this paper, corporate motives for CSR are explored, along with the notion of an altruistic ethical impulse among business leaders or managers, perhaps motivated by religious beliefs. It is suggested that the formal adoption of CSR by corporations could be associated with the changing personal values of managers and that there may be an association between different industries, the personal values of the managers who work in them and their commitment to CSR. This paper is preparatory to an empirical investigation that will address how corporate social responsibility (CSR) is interpreted and institutionalised by organisations, including an analysis of firms’ perceptions of the boundaries regarding where and to whom their corporate social responsibilities lie.

Formal methods for the development and verification of autonomic IT systems

This chapter explores ways in which rigorous mathematical techniques, termed formal methods, can be employed to improve the predictability and dependability of autonomic computing. Model checking, formal specification, and quantitative verification are presented in the contexts of conflict detection in autonomic computing policies, and of implementation of goal and utility-function policies in autonomic IT systems, respectively. Each of these techniques is illustrated using a detailed case study, and analysed to establish its merits and limitations. The analysis is then used as a basis for discussing the challenges and opportunities of this endeavour to transition the development of autonomic IT systems from the current practice of using ad-hoc methods and heuristic towards a more principled approach. © 2012, IGI Global.