The transformational implementation of JSD process specifications via finite automata representation

Conventional structured methods of software engineering are often based on the use of functional decomposition coupled with the Waterfall development process model. This approach is argued to be inadequate for coping with the evolutionary nature of large software systems. Alternative development paradigms, including the operational paradigm and the transformational paradigm, have been proposed to address the inadequacies of this conventional view of software developement, and these are reviewed. JSD is presented as an example of an operational approach to software engineering, and is contrasted with other well documented examples. The thesis shows how aspects of JSD can be characterised with reference to formal language theory and automata theory. In particular, it is noted that Jackson structure diagrams are equivalent to regular expressions and can be thought of as specifying corresponding finite automata. The thesis discusses the automatic transformation of structure diagrams into finite automata using an algorithm adapted from compiler theory, and then extends the technique to deal with areas of JSD which are not strictly formalisable in terms of regular languages. In particular, an elegant and novel method for dealing with so called recognition (or parsing) difficulties is described,. Various applications of the extended technique are described. They include a new method of automatically implementing the dismemberment transformation; an efficient way of implementing inversion in languages lacking a goto-statement; and a new in-the-large implementation strategy.

The debate on human automatism in mid-Victorian England

During the 1830s, Marshall Hall carried out innumerable experiments on a great variety of animals to establish the concept of a ‘reflex arc’. In France F.L.Goltz showed that decerebrate frogs were still capable of complex behaviours. Thomas Laycock in England and Ivan Sechenov in Russia sought to apply the reflex idea to the brain. This paper follows the debate in the periodical literature of mid-Victorian England and discusses the contributions of WB Carpenter, Herbert Spencer, TH Huxley, W Clifford and others. The previous outing of this issue in the post-Cartesian seventeenth century had been largely suppressed by ecclesiastical authority. In the nineteenth century ecclesiastical power had waned, at least in England, and the debate could take a more open form. As neurophysiology and behavioural science developed, with the widespread acceptance of Darwinian evolution, it became more and more difficult to deny that brain and mind were part of the natural world and subject to the usual laws of cause and effect. This, of course, had powerful implications for the human self-image and for jurisprudence. These implications are still with us and the work of neurophysiologists such as Benjamin Libet have only reinforced them. Should humans be regarded as ‘automata’ and, if so, what becomes of ‘free will’, ‘responsibility’, and the rule of law? The Victorian debate is still useful and relevant.

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.

Timing continuous or discontinuous movements across effectors specified by different pacing modalities and intervals

Sensorimotor synchronization is hypothesized to arise through two different processes, associated with continuous or discontinuous rhythmic movements. This study investigated synchronization of continuous and discontinuous movements to different pacing signals (auditory or visual), pacing interval (500, 650, 800, 950 ms) and across effectors (non-dominant vs. non-dominant hand). The results showed that mean and variability of asynchronization errors were consistently smaller for discontinuous movements compared to continuous movements. Furthermore, both movement types were timed more accurately with auditory pacing compared to visual pacing and were more accurate with the dominant hand. Shortening the pacing interval also improved sensorimotor synchronization accuracy in both continuous and discontinuous movements. These results show the dependency of temporal control of movements on the nature of the motor task, the type and rate of extrinsic sensory information as well as the efficiency of the motor actuators for sensory integration.

Bromocriptine:old drug, new formulation and new indication

Bromocriptine is an ergot alkaloid dopamine D receptor agonist that has been used extensively in the past to treat hyperprolactinaemia, galactorrhoea and Parkinsonism. It is known that hypothalamic hypodopaminergic states and disturbed circadian rhythm are associated with the development of insulin resistance, obesity and diabetes in animals and humans. When administered in the early morning at the start of the light phase, a new quick release (QR) formulation of bromocriptine appears to act centrally to reset circadian rhythms of hypothalamic dopamine and serotonin and improve insulin resistance and other metabolic abnormalities. Phase II and III clinical studies show that QR-bromocriptine lowers glycated haemoglobin by 0.6-1.2% (7-13 mmol/mol) either as monotherapy or in combination with other antidiabetes medications. Apart from nausea, the drug is well tolerated. The doses used to treat diabetes (up to 4.8 mg daily) are much lower than those used to treat Parkinson's disease and have not been associated with retroperitoneal fibrosis or heart valve abnormalities. QR-bromocriptine (Cycloset™) has recently been approved in the USA for the treatment of type 2 diabetes mellitus (T2DM). Thus, a QR formulation of bromocriptine timed for peak delivery in the early morning may provide a novel neurally mediated approach to the control of hyperglycaemia in T2DM. © 2010 Blackwell Publishing Ltd.

The effects of ownership and stock liquidity on the timing of repurchase transactions

We analyze detailed monthly data on U.S. open market stock repurchases (OMRs) that recently became available following stricter disclosure requirements. We find evidence that OMRs are timed to benefit non-selling shareholders. We present evidence that the profits to companies from timing repurchases are significantly related to ownership structure. Institutional ownership reduces companies' opportunities to repurchase stock at bargain prices. At low levels, insider ownership increases timing profits and at high levels it reduces them. Stock liquidity increases profits from timing OMRs.

Improving “last mile” delivery performance to retailers in hub and spoke distribution systems

Purpose – The purpose of this paper is to investigate the “last mile” delivery link between a hub and spoke distribution system and its customers. The proportion of retail, as opposed to non-retail (trade) customers using this type of distribution system has been growing in the UK. The paper shows the applicability of simulation to demonstrate changes in overall delivery policy to these customers. Design/methodology/approach – A case-based research method was chosen with the aim to provide an exemplar of practice and test the proposition that simulation can be used as a tool to investigate changes in delivery policy. Findings – The results indicate the potential improvement in delivery performance, specifically in meeting timed delivery performance, that could be made by having separate retail and non-retail delivery runs from the spoke terminal to the customer. Research limitations/implications – The simulation study does not attempt to generate a vehicle routing schedule but demonstrates the effects of a change on delivery performance when comparing delivery policies. Practical implications – Scheduling and spreadsheet software are widely used and provide useful assistance in the design of delivery runs and the allocation of staff to those delivery runs. This paper demonstrates to managers the usefulness of investigating the efficacy of current design rules and presents simulation as a suitable tool for this analysis. Originality/value – A simulation model is used in a novel application to test a change in delivery policy in response to a changing delivery profile of increased retail deliveries.

Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point

Even simple hybrid automata like the classic bouncing ball can exhibit Zeno behavior. The existence of this type of behavior has so far forced a large class of simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad-hoc restrictions to circumvent Zeno behavior or to abandon hybrid automata. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independent of the occurrence of a given event. Such an event can then even occur an unbounded number of times. This insight makes it possible to handle some types of Zeno behavior. If the post-Zeno state is defined explicitly in the given model of the hybrid automaton, the computed enclosure covers the corresponding trajectory that starts from the Zeno point through a restarted evolution.