Determining the specification of a control system from that of its environment

Well understood methods exist for developing programs from given specifications. A formal method identifies proof obligations at each development step: if all such proof obligations are discharged, a precisely defined class of errors can be excluded from the final program. For a class of closed systems such methods offer a gold standard against which less formal approaches can be measured. For open systems -those which interact with the physical world- the task of obtaining the program specification can be as challenging as the task of deriving the program. And, when a system of this class must tolerate certain kinds of unreliability in the physical world, it is still more challenging to reach confidence that the specification obtained is adequate. We argue that widening the notion of software development to include specifying the behaviour of the relevant parts of the physical world gives a way to derive the specification of a control system and also to record precisely the assumptions being made about the world outside the computer.

SimuMap: a computational system for spatial modelling

The paper presents a computational system based upon formal principles to run spatial models for environmental processes. The simulator is named SimuMap because it is typically used to simulate spatial processes over a mapped representation of terrain. A model is formally represented in SimuMap as a set of coupled sub-models. The paper considers the situation where spatial processes operate at different time levels, but are still integrated. An example of such a situation commonly occurs in watershed hydrology where overland flow and stream channel flow have very different flow rates but are highly related as they are subject to the same terrain runoff processes. SimuMap is able to run a network of sub-models that express different time-space derivatives for water flow processes. Sub-models may be coded generically with a map algebra programming language that uses a surface data model. To address the problem of differing time levels in simulation, the paper: (i) reviews general approaches for numerical solvers, (ii) considers the constraints that need to be enforced to use more adaptive time steps in discrete time specified simulations, and (iii) scaling transfer rates in equations that use different time bases for time-space derivatives. A multistep scheme is proposed for SimuMap. This is presented along with a description of its visual programming interface, its modelling formalisms and future plans. (C) 2003 Elsevier Ltd. All rights reserved.

The relationship of cervical joint position error to balance and eye movement disturbances in persistent whiplash

Cervical joint position error (JPE) has been used as a measure of cervical afferent input to detect disturbances in sensori-motor control as a possible contributor to a neck pain syndrome. This study aimed to investigate the relationship between cervical JPE, balance and eye movement control. It was of particular interest whether assessment of cervical ME alone was sufficient to signal the presence of disturbances in the two other tests. One hundred subjects with persistent whiplash-associated disorders (WADs) and 40 healthy controls subjects were assessed on measures of cervical JPE, standing balance and the smooth pursuit neck torsion test (SPNT). The results indicated that over all subjects, significant but weak-to-moderate correlations existed between all comfortable stance balance tests and both the SPNT and rotation cervical ME tests. A weak correlation was found between the SPNT and right rotation cervical JPE. An abnormal rotation cervical JPE score had a high positive prediction value (88%) but low sensitivity (60%) and specificity (54%) to determine abnormality in balance and or SPNT test. The results suggest that in patients with persistent WAD, it is not sufficient to measure ME alone. All three measures are required to identify disturbances in the postural control system. (C) 2005 Elsevier Ltd. All rights reserved.

Functional analysis of a real-time protocol for networked control systems

Traditional real-time control systems are tightly integrated into the industrial processes they govern. Now, however, there is increasing interest in networked control systems. These provide greater flexibility and cost savings by allowing real-time controllers to interact with industrial processes over existing communications networks. New data packet queuing protocols are currently being developed to enable precise real-time control over a network with variable propagation delays. We show how one such protocol was formally modelled using timed automata, and how model checking was used to reveal subtle aspects of the control system's dynamic behaviour.