Verifying data refinements using a model checker

In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.

Continuous action system refinement

Action systems are a framework for reasoning about discrete reactive systems. Back, Petre and Porres have extended these action systems to continuous action systems, which can be. used to model hybrid systems. In this paper we define a refinement relation, and develop practical data refinement rules for continuous action systems. The meaning of continuous action systems is expressed in terms of a mapping from continuous action systems to action systems. First, we present a new mapping from continuous act ion systems to action systems, such that Back's definition of trace refinement is correct with respect to it. Second, we present a stream semantics that is compatible with the trace semantics, but is preferable to it because it is more general. Although action system trace refinement rules are applicable to continuous action systems with a stream semantics, they are not complete. Finally, we introduce a new data refinement rule that is valid with respect to the stream semantics and can be used to prove refinements that are not possible in the trace semantics, and we analyse the completeness of our new rule in conjunction with the existing trace refinement rules.

Semantic properties of μ-charts

μ-Charts are a Statechart-like language which is designed for specifying reactive systems. This paper extends the language of μ-charts with a new parallel operator; it defines a formal semantics for the language, and then it explores the semantic properties of the extended language. The paper concludes with a simple case study to illustrate how the language may be used to specify and reason about reactive systems.

Deceleration affects anticipatory and reactive components of triggered postural responses

Understanding the physiological and psychological factors that contribute to healthy and pathological balance control in man has been made difficult by the confounding effects of the perturbations used to test balance reactions. The present study examined how postural responses were influenced by the acceleration-deceleration interval of an unexpected horizontal translation. Twelve adult males maintained balance during unexpected forward and backward surface translations with two different acceleration-deceleration intervals and presentation orders (serial or random). SHORT perturbations consisted of an initial acceleration (peak acceleration 1.3 m s(-2); duration 300 ms) followed 100 ms later by a deceleration. LONG perturbations had the same acceleration as SHORT perturbations, followed by a 2-s interval of constant velocity before deceleration. Surface and intra-muscular electromyography (EMG) from the leg, trunk, and shoulder muscles were recorded along with motion and force plate data. LONG perturbations induced larger trunk displacements compared to SHORT perturbations when presented randomly and larger EMG responses in proximal and distal muscles during later (500-800 ms) response intervals. During SHORT perturbations, activity in some antagonist muscles was found to be associated with deceleration and not the initial acceleration of the support surface. When predictable, SHORT perturbations facilitated the use of anticipatory mechanisms to attenuate early (100-400 ms) EMG response amplitudes, ankle torque change and trunk displacement. In contrast, LONG perturbations, without an early deceleration effect, did not facilitate anticipatory changes when presented in a predictable order. Therefore, perturbations with a short acceleration-deceleration interval can influence triggered postural responses through reactive effects and, when predictable with repeated exposure, through anticipatory mechanisms.

A Reactive Agent-based Neural Network Car Following Model

This paper presented a novel approach to develop car following models using reactive agent techniques for mapping perceptions to actions. The results showed that the model outperformed the Gipps and Psychophysical family of car following models. The standing of this work is highlighted by its acceptance and publication in the proceedings of the International IEEE Conference on Intelligent Transportation Systems (ITS), which is now recognised as the premier international conference on ITS. The paper acceptance rate to this conference was 67 percent. The standing of this paper is also evidenced by its listing in international databases like Ei Inspec and IEEE Xplore. The paper is also listed in Google Scholar. Dr Dia co-authored this paper with his PhD student Sakda Panwai.