Using Hybrid Automata to Support Human Factors Analysis in a Critical System.
A characteristic that many emerging technologies and interaction techniques have in common is a shift towards tighter coupling between human and computer. In addition to traditional discrete interaction, more continuous interaction techniques, such as gesture recognition, haptic feedback and animation, play an increasingly important role. Additionally, many supervisory control systems (such as flight deck systems) already have a strong continuous element. The complexity of these systems and the need for rigorous analysis of the human factors involved in their operation leads us to examine formal and possibly automated support for their analysis. The fact that these systems have important temporal aspects and potentially involve continuous variables, besides discrete events, motivates the application of hybrid systems modelling, which has the expressive power to encompass these issues. Essentially, we are concerned with human-factors related questions whose answers are dependent on interactions between the user and a complex, dynamic system.In this paper we explore the use of hybrid automata, a formalism for hybrid systems, for the specification and analysis of interactive systems. To illustrate the approach we apply it to the analysis of an existing flight deck instrument for monitoring and controlling the hydraulics subsystem.
Introduction
The distinguishing feature of the modelling and specification of interactive systems is
the need to accommodate the user; for example, to formalise and analyse user require-
ments, and to conduct usability reasoning. The environment can also play a significant
role, as it can impose constraints on both the system and the user, and the communication
paths between them.
In existing approaches, interaction between user and system is assumed to be of a
discrete and sequential nature. Such a view may be inadequate where interaction between
user, system and environment contains continuous as well as discrete elements.
The 'continuous' aspect of the system can take many forms, including, but not restricted
to, continuous input and output devices. Certain types of interactive system have always
had a hybrid element - for example many forms of supervisory control systems, such
as flight deck systems and medical monitoring systems. Additionally, many emerging
technologies, such as virtual reality and haptic input devices, support richer and more
continuous interaction with the user, and hence applications using such techniques can
also be viewed as hybrid systems [18].
If the models we build of such systems are to support reasoning about issues of usability
and user requirements, then building a model of system behaviour is not enough
- we must also have some means of referring to both the user and the environment. It
has been proposed that usability issues can be better understood in terms of the conjoint
behaviour of system and user, and that syndetic models [8, 7, 9], which combine a formal
system model with a representation of human cognition, support such an approach.
In this paper, we do not consider the modelling of human cognition but rather apply
models of user input and observation of system output, which afford the possibility of
reasoning about user behaviour and inference. These models can take the form of constraints
imposed by the limitations of the user or of the environment, or they may take
the form of more explicit models of relevant aspects of the user or environment.
Automata provide a relatively simple formalism, with a convenient graphical repre-
sentation, for specifying the behaviour of systems. Basically, an automaton consists of
a number of locations, and a number of transitions which link these locations. System
specifications typically involve several automata, synchronised on certain transitions.
They include variables on which location invariants and transition guards are based.
Recently, a number of interesting variants of automata, including timed and hybrid au-
tomata, have been developed that allow the specification of processes that evolve in a
continuous rather than a discrete way. Timed automata include real valued clock variables
which increase at a uniform rate [14, 3]. Hybrid automata [11], on which we focus
in this paper, include analog variables which can change at arbitrary rates (both positive
and negative). The continuous change of real valued variables in hybrid automata
is specified by sets of differential equations, as is common practice in for example
physics. The automata based formalisms do not only provide a specification language
with a graphical interpretation, but also allow for automatic verification of properties
by means of reachability analysis provided by several model checking tools [3, 14, 12].
The example we focus on concerns flight deck instrumentation concerning the hydraulics
subsystem of an aircraft. This is based on a case study originally presented by
Fields and Merriam [10], which involves analysis of the support the instrument provides
to the user for the diagnosis of system failures (including issues of representation). Two
goals are identified in relation to this activity; firstly to preserve the safety of the system
(maintaining hydraulic power to the control surfaces), and secondly to discover the
cause of a problem. The user's actions are hence closely tied with the process of reasoning
about the possible faults in the system. As noted in [10], this type of activity is
typical in process control settings, and hence we see the case study as representative of
a class of applications. Through the use of hybrid automata, we have the potential to
expand on the original analysis, not only by modelling timing constraints, but also the
continuous variables representing quantities in the hydraulics subsystem itself.
Case study on aircraft hydraulics
The case study we analyse in this paper is taken from the domain of aircraft hydraulics,
and is based on the description in [10]. The hydraulics system is vital to the safe operation
of the system as it is the means by which inputs from the the pilot or autopilot are
conveyed to the control surfaces (eg. rudder and ailerons). Movement of the surfaces
is achieved by servodynes which rely on hydraulic fluid. This fluid is supplied from
reservoirs, and a number of valves determine which reservoir supplies a given servo-
dyne. In [10] a generic model of hydraulic systems is first presented, and a simplified
(but realistic) version used as the basis of analysis. We base our treatment on the simple
model.
In the simple case, only two control surfaces - rudder and aileron - are included. The
operation of these surfaces is powered by servodynes; each surface has a primary and
secondary servodyne. Hydraulic fluid is supplied to the servodynes from two reservoirs,
the primary servodynes of each being connected to the blue reservoir, the secondary to
the green reservoir. The valves between the reservoirs and servodynes are such that each
surface is connected to only one tank at a time (see Fig. 1).
Blue
Reservoir
Green
Reservoir
Rudder
Aileron
Fig. 1. Hydraulic System, from [10]
The focus of the model is the diagnosis and minimisation of leaks by the human
operator, the motivation being that a control surface connected to an empty reservoir
cannot be operated and hence is a serious hazard. In the model, each reservoir can leak
independently, as can each of the servodynes. Failures can occur in any combination of
reservoirs and servodynes, although fluid is only lost through a leaky servodyne while
the valve connecting it to one of the reservoirs is open. In reality there are many other
components involved in the system, and many more possible types of system failure,
but the model described here suffices to illustrate our approach.
User operation of the system is by means of two switches, one for each control
surface, which can be set by the user to either blue or green (see Fig. 2(a)). The level of
fluid in each reservoir is presented to the user by means of a pie-chart like display (see
Fig. 2(b)), where the loss of fluid can be observed by the pilot as a gradually decrease
of the 'filled' portion of arc in the display (shaded grey in our diagram).
Green
Blue
Rudder Aileron
(b)
(a)
Blue Green
Fig. 2. Controls and status display, adapted from [10]
The case study is interesting since it includes both real-time issues surrounding the
diagnosis and correction of leaks. There are analog (continuous) variables representing
the fluid levels in the tanks (which can change continuously at various rates), and the
continuous representation of those levels by the level indicators on the flight deck. These
continuous aspects are combined with discrete controls operated by the pilot or flight
engineer.
To illustrate how the diagnosis of leaks is tied to the observation of tank levels in the
different switch configurations, consider the following scenario, where the rudder primary
(R1) and aileron secondary (A2) servodynes are leaking. The sequence of switch
settings, observations, and the 'ideal' user understanding of the system involved in the
diagnosis are illustrated in table 1. Initially the user observes a decrease (L) in the quantity
of the blue reservoir (BR) and no decrease (N) in the level of the green reservoir
(GR). Setting both switches to green, a decrease in the level of the green reservoir is
observed, leading to the conclusion that neither blue nor green reservoir are leaking.
Setting the rudder back to blue leads to loss from both reservoirs, leading to the conclusion
that both the rudder primary and aileron secondary servodynes are leaking, and
toggling both switches leads the user to conclude that neither rudder secondary nor
aileron primary are leaking, completing the users knowledge of the state of the system.
Step Control State Observation Possible causes of leak
Rudder Aileron Blue Green

Table

1. Observations and inferences
3 Hybrid automata
In this section we give an informal overview of the specification language for hybrid
automata HyTech and the analysis capabilities of the associated tools. For details on
the formalism, the use of the tools and for further references to articles on the theory
underlying HyTech we refer to [12, 11].
3.1 HyTech specification language
A HyTech specification consists of a number of automata, a set of variable declarations
and a number of analysis commands. Each automaton is named, and contains some
initial conditions, a set of locations (with invariants), a set of transitions (which may
include guards and variable assignments), some of which may be labelled as urgent.
Transitions may be synchronised between any number of automata (multi-part syn-
chronisation), and variables are global, i.e. they may be referenced from any automaton.
Four forms of real-valued variable are provided, each of which is distinguished by the
rate of change. Discrete variables are 'ordinary' variables which can be assigned values,
and which have a rate of zero. Clocks are as discrete variables but increase at a constant
rate of 1. Stopwatches may have a rate of either zero or 1. Analog variables form the
general case and arbitrary linear conditions may be placed on their rate of change. a
state of a HyTech specification consists of a location vector and a valuation. The location
vector consists of one location name of every automaton in the specification. A
valuation is a vector of real numbers, containing a value for each of the global variables
of the specification.
Graphical manipulation of HyTech specifications is possible via the AutoGraph
tool, and a converter which maps state transition diagrams in AutoGraph to the HyTech
textual specification language [13].
3.2 HyTech model checking
Besides a specification language based on automata HyTech provides a tool for reachability
analysis. With the tool a subclass of hybrid automata specifications can be automatically
analysed. This subclass is the set of linear hybrid automata. These are hybrid
automata in which all invariants and conditions are expressed as (finite) conjunctions of
linear predicates. A linear predicate is an (in)equality between linear terms such as for
example:
The coefficients in the predicates must be rationals. HyTech can compute the set of
states of the parallel composition of linear hybrid automata. Given an initial region (a
subset of the state space is called a region) 1 , it can compute the set of states that is
reachable from the initial region by forward reachability analysis. Conversely, given a
final set of states, it can compute the set of states from which the final region can be
reached by using backward reachability analysis. As a side effect of reachability analysis
a sequence of delay- and transition steps can be generated that shows an example
of how one set of states can be reached starting from another. This can be extremely
helpful for what we could call 'high-level debugging' of a formal model of a system.
A third analysis feature is the use of models that contain parameters. HyTech can
be used to synthesize automatically precise constraints on these parameters which are
necessary to satisfy certain properties. In later sections we show how these kinds of
analysis can be useful for the analysis of human computer interfaces.
3.3 Example
Presented in Fig. 3 is an example of two simple automata, one modelling a reservoir
(Res) and one modelling an observer which monitors the level of liquid in the reservoir
(Observe). The automaton Res models the operation of a reservoir in the hydraulics
1 Note that in the context of HyTech specifications, the term region is used to refer to an arbitrary
subset of the state space; in the underlying theory concerning model checking of automata
specifications, this term has a more specific meaning.
system, and includes three locations encapsulating the possible states of the reservoir,
namely that it is not empty and not leaking (RNL), that it is leaking (RL) and that it is
empty (emptyR). It is assumed that we have defined two variables. The analog variable
that indicates the level of the liquid in the reservoir and discrete variable red
modelling a red lamp that can be on (red=1) or off (red=0).
The automaton Res starts in the initial state indicated by a double circle and with
the start condition, indicated at label Start, that the liquid level g in the reservoir is
3. In the initial state two invariant conditions hold. One states that the reservoir should
contain liquid (g>=0) and the other stating that the the reservoir is not leaking, i.e. the
rate with which the level changes is zero (dg=0). Eventually the reservoir may start
leaking. This is modelled by the transition from RNL to RL. The reservoir enters a state
in which the reservoir is not empty and is leaking with a rate of 1 unit per time-unit
(dg=-1). When the reservoir is empty, the automaton is forced to leave location RL,
because it can only stay there as long as g>=0, and moves to location emptyR by a
transition labeled by emptyr.
The automaton Observe models the detection of the reservoir becoming empty
and signalling this by means of a red light indicator (red'=1). When automaton Res
performs the transition labeled by emptyr, automaton Observe synchronises on this
label and moves to location o2. After this it performs the next transition as soon as
possible because of the special label asap which denotes that it is an urgent transition,
and switches the red light on (red'=1).
Res Res Res Res ResResResResRes Res Res Res Res Res Res
Res Res
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Start: g=3
Observe Observe Observe Observe ObserveObserveObserveObserveObserve Observe Observe Observe Observe
Observe Observe Observe Observe
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
Start: red=0
RNL RNL RNL RNL RNLRNLRNLRNLRNL RNL RNL RNL RNL RNL
RNL RNL RNL
dg=0 dg=0 dg=0
RL RL RL RL RLRLRLRLRL RL RL RL RL RL RL
RL RL
emptyR emptyR emptyR emptyR emptyRemptyRemptyRemptyRemptyR emptyR emptyR emptyR emptyR emptyR emptyR emptyR emptyR
dg=0 dg=0 dg=0 dg=0 dg=0dg=0dg=0dg=0dg=0 dg=0 dg=0 dg=0 dg=0 dg=0 dg=0 dg=0 dg=0
emptyr emptyr emptyr emptyr emptyremptyremptyremptyremptyr emptyr emptyr emptyr emptyr emptyr emptyr
emptyr emptyr
emptyr emptyr emptyr emptyr emptyremptyremptyremptyremptyr emptyr emptyr emptyr emptyr emptyr emptyr
emptyr emptyr
red'=1 red'=1 red'=1 red'=1 red'=1red'=1red'=1red'=1red'=1 red'=1 red'=1 red'=1 red'=1 red'=1
red'=1 red'=1 red'=1
asap asap asap asap asapasapasapasapasap asap asap asap asap asap
asap asap asap
Fig. 3. Reservoir Automaton and Detection of Emptyness
4 Reasoning about interactive systems with HyTech
The approach we take is to model not only the system but also aspects of the user and
potentially the environment by means of various automata. For the moment, we consider
user models which consist of models for input, and possibly observation. An input
model could simply capture the possible sequences of operations a user can invoke, or
it can be more focussed towards a specific task, or even a strategy for achieving some
goal.
The potential for applying these specifications to usability reasoning derives from
the way in which the user and system automata execute together, and hence it is worth
considering how the models are composed.
4.1 Linking user and system models
There are a number of ways in which the user and system automata can be linked:
synchronisation transitions, including urgent transitions. Where transitions are synchronised
(they have the same label), then they must occur simultaneously in all
automata which contain the label. Thus by means of a synchronised transition, we
can require that both system and user models make a transition at the same time.
shared variables - use of a variable from another part of the model in a guard or
invariant corresponds to an observation of some form. Hence where the user model
references the value of a system variable, this corresponds to the user observing the
variable - presumably in the presentation of the system.
The specification may also enforce constraints on the reachable states of the automata
which are less obvious, for example mutually exclusive system and user states. While
these relationships must be encoded at some level by means of synchronisations or
guards, they can be subtle and difficult to perceive. When we consider the significance
of such relationships to usability reasoning, we find that there are a number of interesting
semantic issues. For example, what does it mean when one "waits" for the other.
This seems to be an issue of initiative. Also, there can be a distinction between the occurrence
of an event, for example in the system model, and perception of that event,
which might correspond to a transition in the user model. Consider for example a form
of 'polling' behaviour by a user who periodically checks some portion of the system
display, rather than continuously monitoring it (an assumption which would be unreasonable
in many application domains).
The analysis section of the specification may also contain abstractions which can
be seen as modelling aspects of the user - eg. a region definition may correspond to
observation of the state of the system by the user. A detailed example of this is given in
section 6.3.
4.2 Properties
There are many benefits associated with the construction of a formal specification, but
the one we focus on here is the possibility of formally verifying whether certain properties
hold on the combined specification of system, user, and environment, in this case
via the capabilities of the HyTech model-checker. The basic capabilities of HyTech are
based on reachability analysis, but there are a number of ways in which this can be used
in the context of human factors analysis:
simple reachability This analysis technique can be used to show that it is possible for
the system to reach desirable states or sets of states (for example those representing
the user's goals), and that it is impossible to reach undesirable states (for example
those which would compromise the safety of the system). Abstractions such as
impact, i.e. 'the effect that an action or sequence of actions has on the safe and
successful operation of the system' [4] can be formalised and checked by means of
such reachability properties.
state/display conformance Where we have automata representing the presentation
of the system state, or observation of this by the user, we can check conformance
between the automata representing the system state, and those representing the presentation
and/or observation. See for example Dix [6] for a discussion of various
forms of state-display conformance.
performance related properties Since we can derive limits on timed and analog variables
such that certain states are reachable for example, it is possible to examine
performance related issues such as latency (see [1] for a treatment of latency related
issues in a lip synchronisation protocol modelled in UPPAAL, a specification
language for timed automata). Data on latencies can be compared to human factors
and ergonomics data on human response times and perception thresholds, to
ascertain whether system performance is compatible with the user's capabilities.
A review of the use of machine assisted verification (including model checking) in the
analysis of interactive systems can be found in Campos and Harrison [2]. Rushby [17]
describes some preliminary work in using a model checker to check for inconsistencies
between a user's model of system operation and actual system behaviour which lead to
automation surprises in an avionics case study [16].
5 Hydraulics system specification
In this section, we describe a formal specification of the hydraulics system introduced
in section 2. We construct automata to represent both the system and the user.
5.1 System model
The system model comprises two sets of automata, namely:
- those that model the servodyne leakage and valve state, one for each control surface.
- those that model the reservoirs, one for each reservoir.
We define two valve automata - one for each control surface, ValveR for the rudder
and ValveA for the aileron. The valve for each control surface can be set to either the
blue or green reservoir, and correspondingly the primary or secondary servodyne. These
transitions are given synchronisation labels sab, signifying 'set aileron to blue', srg
signifying 'set rudder to green', and so on. The locations with a label containing a B
as the second letter are those where the blue reservoir has been selected, and those
containing a G where the green reservoir has been selected.
Furthermore, each servodyne can leak independently, yielding a total of eight locations
for each automaton. From a given situation, more leaks can occur, and so we have
transitions (unlabelled in Fig. 4) denoting the occurrence of (additional) leaks. These
leaks are indicated in the location names by the last two letters, each of which can be
either N - notleaking or L - leaking, the second last letter representing the state of the
primary (blue) servodyne and the last letter that of the secondary (green) servodyne.
For each valve of the aileron an analog variable is introduced that models the rate
of leaking of the connected servodyne. For the servodynes of the aileron variables ba
and ga model the amount of fluid leaking from the primary and the secondary aileron
servodyne respectively, and their first time derivatives dba and dga the respective rate
of leakage. Note that when the valve connecting a leaky servodyne is closed the servo-
dyne does not loose liquid. So, for example, in the location labelled by AGLL, standing
for the aileron switched to the green (secondary) servodyne where both servodynes are
leaking, only the derivative regarding the leak in the secondary servodyne is non zero
(dba=0, dga=1).
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
ABNN ABNN ABNN ABNN ABNNABNNABNNABNNABNN ABNN ABNN ABNN ABNN
ABNN ABNN ABNN ABNN
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
AGNN AGNN AGNN AGNN AGNNAGNNAGNNAGNNAGNN AGNN AGNN AGNN AGNN AGNN AGNN
AGNN AGNN
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
AGLN AGLN AGLN AGLN AGLNAGLNAGLNAGLNAGLN AGLN AGLN AGLN AGLN
AGLN AGLN AGLN AGLN
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
ABLN ABLN ABLN ABLN ABLNABLNABLNABLNABLN ABLN ABLN ABLN ABLN ABLN ABLN
ABLN ABLN
dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0dba=1,dga=0dba=1,dga=0dba=1,dga=0dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0
ABLL ABLL ABLL ABLL ABLLABLLABLLABLLABLL ABLL ABLL ABLL ABLL ABLL
ABLL ABLL ABLL
dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0dba=1,dga=0dba=1,dga=0dba=1,dga=0dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0
dba=1,dga=0 dba=1,dga=0 dba=1,dga=0
AGLL AGLL AGLL AGLL AGLLAGLLAGLLAGLLAGLL AGLL AGLL AGLL AGLL AGLL AGLL AGLL AGLL
ABNL ABNL ABNL ABNL ABNLABNLABNLABNLABNL ABNL ABNL ABNL ABNL
ABNL ABNL ABNL ABNL
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
AGNL AGNL AGNL AGNL AGNLAGNLAGNLAGNLAGNL AGNL AGNL AGNL AGNL AGNL
AGNL AGNL AGNL
sag sag sag sag sagsagsagsagsag sag sag sag sag sag
sag sag sag
sab sab sab sab sabsabsabsabsab sab sab sab sab sab
sab sab sab sab sab sab sab sabsabsabsabsab sab sab sab sab sab
sab sab sab
sag sag sag sag sagsagsagsagsag sag sag sag sag
sag sag sag sag
sag sag sag sag sagsagsagsagsag sag sag sag sag sag
sag sag sag sab sab sab sab sabsabsabsabsab sab sab sab sab sab
sab sab sab
sag sag sag sag sagsagsagsagsag sag sag sag sag
sag sag sag sag
sab sab sab sab sabsabsabsabsab sab sab sab sab
sab sab sab sab
Fig. 4. Aileron Valve Automaton
A similar automaton is constructed for the valves and servodynes of the rudder with
variables br and gr, see Fig. 7.
The reservoir automaton, as presented in Fig. 5, includes three locations indicating
the status of the reservoir which can be empty, leaking, and not leaking but not
empty. For the green reservoir these have labels emptyG, GRL and GRN respectively.
Associated with the locations we have both invariants on the continuous variable g (the
GreenRes GreenRes GreenRes GreenRes GreenResGreenResGreenResGreenResGreenRes GreenRes GreenRes GreenRes GreenRes
GreenRes GreenRes GreenRes GreenRes
GRNL GRNL GRNL GRNL GRNLGRNLGRNLGRNLGRNL GRNL GRNL GRNL GRNL GRNL GRNL
GRNL GRNL
dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dgadg=0-dgr-dgadg=0-dgr-dgadg=0-dgr-dgadg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga
GRL GRL GRL GRL GRLGRLGRLGRLGRL GRL GRL GRL GRL
GRL GRL GRL GRL
emptyG emptyG emptyG emptyG emptyGemptyGemptyGemptyGemptyG emptyG emptyG emptyG emptyG
emptyG emptyG emptyG emptyG
dg=0 dg=0 dg=0 dg=0 dg=0dg=0dg=0dg=0dg=0 dg=0 dg=0 dg=0 dg=0
dg=0 dg=0 dg=0 dg=0
Fig. 5. Reservoir Automaton
level of fluid in the reservoir) and conditions on the rate variable dg, the rate at which
fluid is lost being the sum of that lost from the servodynes connected to the green reservoir
(-dgr-dga) and leakage from the reservoir itself (-1 in the condition for location
GRL). When the reservoir is empty, both the level of fluid and the rate of leakage are
zero.
A similar automaton is constructed for the blue reservoir, see Fig. 7.
5.2 User model
We model user input by means of a single automaton, in which the user can perform
actions to move between the four possible combinations of switch settings; that both
rudder and aileron are set to blue RBAB, that rudder is set to green and aileron to blue
RGAB and so on, as illustrated in Fig. 6. The transitions have synchronisation labels
that establish synchronisation between user actions and the two valves. Each transition
is guarded by a constraint on the level of fluid in the reservoir to which the user wants
to connect a servodyne.
RBAB RBAB RBAB RBAB RBABRBABRBABRBABRBAB RBAB RBAB RBAB RBAB
RBAB RBAB RBAB RBAB RBAG RBAG RBAG RBAG RBAGRBAGRBAGRBAGRBAG RBAG RBAG RBAG RBAG
RBAG RBAG RBAG RBAG
RGAB RGAB RGAB RGAB RGABRGABRGABRGABRGAB RGAB RGAB RGAB RGAB RGAB
RGAB RGAB RGAB RGAG RGAG RGAG RGAG RGAGRGAGRGAGRGAGRGAG RGAG RGAG RGAG RGAG RGAG
RGAG RGAG RGAG
User User User User UserUserUserUserUser User User User User User
User User User
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
srg srg srg srg srgsrgsrgsrgsrg srg srg srg srg srg srg
srg srg
sag sag sag sag sagsagsagsagsag sag sag sag sag sag sag
sag sag
sab sab sab sab sabsabsabsabsab sab sab sab sab sab sab
srg srg srg
srb srb srb srb srbsrbsrbsrbsrb srb srb srb srb srb
srb srb srb
sag sag sag sag sagsagsagsagsag sag sag sag sag sag sag
sag sag
sab sab sab sab sabsabsabsabsab sab sab sab sab
srb srb srb srb srbsrbsrbsrbsrb srb srb srb srb
srb srb srb srb
Fig. 6. User Input Automaton
User observation of the presentation of the system status, i.e. the change in the fluid
level indicators, can also be represented by automata. However for the purpose of the
analysis discussed in this paper it was found simpler and more convenient to model
observation as a set of regions defined in the analysis component of the HyTech spec-
ification. Each region corresponds to a user observationally-equivalent class of states.
Details of this approach are discussed in the next section.
As can be seen in the above diagrams, both valve/servodyne automata and the user
input automaton are synchronised on four events (namely srb, srg, sab, sag), which set
the rudder and aileron valves to the blue or green settings. The complete specification
(without an analysis section) is shown in Fig. 7.
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
GreenRes GreenRes GreenRes GreenRes GreenResGreenResGreenResGreenResGreenRes GreenRes GreenRes GreenRes GreenRes GreenRes GreenRes
GreenRes GreenRes
User User User User UserUserUserUserUser User User User User User User User User
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Config Config Config Config ConfigConfigConfigConfigConfig Config Config Config Config Config Config Config Config
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
var g, gr, ga, b, br, ba: analog;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
t: clock;
BlueRes BlueRes BlueRes BlueRes BlueResBlueResBlueResBlueResBlueRes BlueRes BlueRes BlueRes BlueRes BlueRes BlueRes
BlueRes BlueRes
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
RBNN RBNN RBNN RBNN RBNNRBNNRBNNRBNNRBNN RBNN RBNN RBNN RBNN RBNN
RBNN RBNN RBNN
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
dbr=0, dgr=0
RGNN RGNN RGNN RGNN RGNNRGNNRGNNRGNNRGNN RGNN RGNN RGNN RGNN
RGNN RGNN RGNN RGNN
dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0
dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0
RGLN RGLN RGLN RGLN RGLNRGLNRGLNRGLNRGLN RGLN RGLN RGLN RGLN
RGLN RGLN RGLN RGLN
dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0
dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0
RBLN RBLN RBLN RBLN RBLNRBLNRBLNRBLNRBLN RBLN RBLN RBLN RBLN RBLN
RBLN RBLN RBLN
dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0dbr=1,dgr=0dbr=1,dgr=0dbr=1,dgr=0dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0
dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0
GRNL GRNL GRNL GRNL GRNLGRNLGRNLGRNLGRNL GRNL GRNL GRNL GRNL GRNL GRNL GRNL GRNL
dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dgadg=0-dgr-dgadg=0-dgr-dgadg=0-dgr-dgadg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga dg=0-dgr-dga
GRL GRL GRL GRL GRLGRLGRLGRLGRL GRL GRL GRL GRL
GRL GRL GRL GRL
RBAB RBAB RBAB RBAB RBABRBABRBABRBABRBAB RBAB RBAB RBAB RBAB RBAB RBAB RBAB RBAB RBAG RBAG RBAG RBAG RBAGRBAGRBAGRBAGRBAG RBAG RBAG RBAG RBAG RBAG RBAG RBAG RBAG
RGAB RGAB RGAB RGAB RGABRGABRGABRGABRGAB RGAB RGAB RGAB RGAB
RGAB RGAB RGAB RGAB RGAG RGAG RGAG RGAG RGAGRGAGRGAGRGAGRGAG RGAG RGAG RGAG RGAG
RGAG RGAG RGAG RGAG
BRNL BRNL BRNL BRNL BRNLBRNLBRNLBRNLBRNL BRNL BRNL BRNL BRNL
BRNL BRNL BRNL BRNL
db=0-dbr-dba db=0-dbr-dba db=0-dbr-dba db=0-dbr-dba db=0-dbr-dbadb=0-dbr-dbadb=0-dbr-dbadb=0-dbr-dbadb=0-dbr-dba db=0-dbr-dba db=0-dbr-dba db=0-dbr-dba db=0-dbr-dba
db=0-dbr-dba db=0-dbr-dba db=0-dbr-dba db=0-dbr-dba
BRL BRL BRL BRL BRLBRLBRLBRLBRL BRL BRL BRL BRL
BRL BRL BRL BRL
RBLL RBLL RBLL RBLL RBLLRBLLRBLLRBLLRBLL RBLL RBLL RBLL RBLL RBLL
RBLL RBLL RBLL
dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0dbr=1,dgr=0dbr=1,dgr=0dbr=1,dgr=0dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0
dbr=1,dgr=0 dbr=1,dgr=0 dbr=1,dgr=0
RGLL RGLL RGLL RGLL RGLLRGLLRGLLRGLLRGLL RGLL RGLL RGLL RGLL RGLL
RGLL RGLL RGLL
RBNL RBNL RBNL RBNL RBNLRBNLRBNLRBNLRBNL RBNL RBNL RBNL RBNL RBNL RBNL RBNL RBNL
dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0 dbr=0,dgr=0
RGNL RGNL RGNL RGNL RGNLRGNLRGNLRGNLRGNL RGNL RGNL RGNL RGNL RGNL RGNL
RGNL RGNL
ABNN ABNN ABNN ABNN ABNNABNNABNNABNNABNN ABNN ABNN ABNN ABNN ABNN ABNN ABNN ABNN
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
AGNN AGNN AGNN AGNN AGNNAGNNAGNNAGNNAGNN AGNN AGNN AGNN AGNN AGNN AGNN AGNN AGNN
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
AGLN AGLN AGLN AGLN AGLNAGLNAGLNAGLNAGLN AGLN AGLN AGLN AGLN
AGLN AGLN AGLN AGLN
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
ABLN ABLN ABLN ABLN ABLNABLNABLNABLNABLN ABLN ABLN ABLN ABLN ABLN ABLN
ABLN ABLN
dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0dba=1,dga=0dba=1,dga=0dba=1,dga=0dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0
ABLL ABLL ABLL ABLL ABLLABLLABLLABLLABLL ABLL ABLL ABLL ABLL ABLL ABLL
dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0dba=1,dga=0dba=1,dga=0dba=1,dga=0dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0 dba=1,dga=0
AGLL AGLL AGLL AGLL AGLLAGLLAGLLAGLLAGLL AGLL AGLL AGLL AGLL AGLL
AGLL AGLL AGLL
ABNL ABNL ABNL ABNL ABNLABNLABNLABNLABNL ABNL ABNL ABNL ABNL ABNL ABNL ABNL ABNL
dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0 dba=0,dga=0
AGNL AGNL AGNL AGNL AGNLAGNLAGNLAGNLAGNL AGNL AGNL AGNL AGNL
AGNL AGNL AGNL AGNL
emptyG emptyG emptyG emptyG emptyGemptyGemptyGemptyGemptyG emptyG emptyG emptyG emptyG emptyG emptyG
dg=0 dg=0 dg=0 dg=0 dg=0dg=0dg=0dg=0dg=0 dg=0 dg=0 dg=0 dg=0 dg=0 dg=0
db=0 db=0 db=0 db=0 db=0db=0db=0db=0db=0 db=0 db=0 db=0 db=0 db=0
db=0 db=0 db=0
srg srg srg srg srgsrgsrgsrgsrg srg srg srg srg srg srg srg srg
sag sag sag sag sagsagsagsagsag sag sag sag sag sag sag sag sag
srg srg srg srg srgsrgsrgsrgsrg srg srg srg srg
srg srg srg srg
sag sag sag sag sagsagsagsagsag sag sag sag sag sag
sag sag sag
srg srg srg srg srgsrgsrgsrgsrg srg srg srg srg srg srg
srg srg
srb srb srb
sab sab sab sab sabsabsabsabsab sab sab sab sab sab sab
srb srb srb srb srbsrbsrbsrbsrb srb srb srb srb srb srb srb srb
sab sab sab sab sabsabsabsabsab sab sab sab sab sab
sab sab sab
srb srb srb srb srbsrbsrbsrbsrb srb srb srb srb srb srb
srb srb srg srg srg srg srgsrgsrgsrgsrg srg srg srg srg srg srg srg srg srb srb srb srb srbsrbsrbsrbsrb srb srb srb srb
srb srb srb srb
srg srg srg srg srgsrgsrgsrgsrg srg srg srg srg srg srg srg srg
srb srb srb srb srbsrbsrbsrbsrb srb srb srb srb srb
srb srb srb
srg srg srg srg srgsrgsrgsrgsrg srg srg srg srg srg
srg srg srg
srb srb srb srb srbsrbsrbsrbsrb srb srb srb srb srb srb srb srb sag sag sag sag sagsagsagsagsag sag sag sag sag
sag sag sag sag
sab sab sab sab sabsabsabsabsab sab sab sab sab
sab sab sab sab sab sab sab sab sabsabsabsabsab sab sab sab sab sab sab sab sab
sag sag sag sag sagsagsagsagsag sag sag sag sag sag sag sag sag
sag sag sag sag sagsagsagsagsag sag sag sag sag
sag sag sag sag sab sab sab sab sabsabsabsabsab sab sab sab sab sab sab sab sab
sag sag sag sag sagsagsagsagsag sag sag sag sag sag sag sag sag
sab sab sab sab sabsabsabsabsab sab sab sab sab
sab sab sab sab
Fig. 7. Complete specification
6 Analysis
Having completed our specification of the system, we proceed with a number of analy-
ses. The examples in the current section serve mainly to illustrate the approach and the
possible kinds of analyses that could be performed with the model checker HyTech to
support human factors analysis. In some cases the results could also have been derived
without assistance of a model checker. However, it is easy to imagine extensions of
the case study in which such analyses are much harder to perform accurately without
automatic analysis.
In addition to the reachability and performance related analysis, we illustrate an
original form of task-driven analysis which concerns the possible inferences to be made
by the user in the diagnosis of system faults. We show how the expressiveness of the
analysis language of HyTech can be exploited to model the observations of the liquid
indicators by the pilot when performing the diagnosis activity. This approach makes
it possible to evaluate and compare the efficiency and efficacy of different diagnosis
strategies.
Our aim in this section is to illustrate how real-time and continuous elements can
be included in analyses with a human factors focus. In particular we show how hybrid
automata and associated model checking tools can support analyses driven by concepts
such as user tasks and user inference, which are external to the system specification.
6.1 Safety conditions
Safety conditions can be expressed via reachability conditions, and checked in a straight-forward
fashion. Sample traces, which reach a target region from an initial region, including
timing information, can be constructed automatically by HyTech. In the context
of our case study, the first simple analysis is to let HyTech find out whether a fix
can be reached starting from a particular 'leaky' situation. For example, let's suppose
the valves are switched to blue and only the primary servodyne of the rudder and the
secondary servodyne of the aileron are leaking. This situation is defined as the region
variable init reg.
init_reg := loc[User]=RBAB &
loc[ValveR]=RBLN &
loc[ValveA]=ABNL &
loc[GreenRes]=GRNL &
loc[BlueRes]=BRNL &
The observation of a decrease in the blue and green reservoir fluid quantity can be
expressed as two regions. Leaking of 'green' fluid can be observed when the rudder
is switched to green and the secondary servodyne is leaking, or when the aileron is
switched to green and the secondary servodyne is leaking or when the green reservoir is
leaking. A similar region can be defined for the observation of a decrease in the 'blue'
fluid.
In HyTech these regions are defined in the following way where j denotes the logical
'or':
green_leak := (loc[ValveR]=RGNL | loc[ValveR]=RGLL |
loc[ValveA]=AGNL | loc[ValveA]=AGLL |
loc[GreenRes]=GRL);
blue_leak := (loc[ValveR]=RBLL | loc[ValveR]=RBLN |
loc[ValveA]=ABLL | loc[ValveA]=ABLN |
loc[BlueRes]=BRL);
We can let HyTech compute the set of states reachable from this initial region intersected
with those states in which no leaks occur (defined as fin reg).
reached := reach forward from init_reg endreach;
If the intersection is not empty, we can let HyTech print a (shortest) trace from the
leaking situation to a situation in which the problem is fixed.
if empty (fin_reg & reached)
then prints "No fix possible";
else print fin_reg & reached;
print trace to fin_reg using reached;
The result is shown below:
Generating trace to specified target region ========
VIA: srg
============ End of trace generation ============
Max memory used
Time spent
The first three lines describe the set of states characterised by the intersection of
fin reg and reached. It consists of a location vector that lists the location of each
automaton in the specification in the situation in which a fix for the leaking is realised.
The list gives only the names of the automata locations. They belong respectively to the
automata ValveR, GreenRes, User, BlueRes and ValveA. The order in which
the location vector is reported is the same in each following analysis in this section.
The next two lines give the conditions on the variables that have to be satisfied in
that case.
The second part of the result concerns the trace starting from the initial region to
the final region. In this case the shortest trace to a fix consists of just one action, namely
switching the rudder to 'green', achieved by transition srg. Since we have not specified
that switching activity performed by the pilot costs time, the transition can be
performed in zero time units. Adding time constraints on the activity of the user could
be an interesting extension of the current case study. Further details on these constraints
should first be studied though in order to keep the model as realistic as possible.
In this case study there are 'leaky' situations that obviously cannot be fixed by the
pilot by means of the switches. One such situation is when both reservoirs are leaking.
Forward reachability analysis of such a situation gives us indeed the answer that a fix is
not possible.
A more interesting question is for which 'leaky' situations a fix can be found. This
can be computed by using a backward reachability analysis, starting from a situation
in which no leaks occur, i.e. the above defined region fin reg. This leads to a set of 36
states. Three representative ones are shown below.
Inspection of all the reported states shows that the automata that model the reservoirs
are always in the non-leaking location (GRNL and BRNL). Moreover, it never
occurs that both valves of the rudder or both valves of the aileron are leaking at the
same time. This gives indeed exactly the conditions under which the pilot is able to find
a fix.
6.2 Constraints on timing and continuous variables
Using HyTech, we can derive limits on the variables, including fluid levels and rates
of leakage. To do this, we use a special type of variable - parameters - and get the
system to find the values of the parameters for which a solution can be found (some
final region reached). For example, consider an analysis where we declare the initial
levels of fluid in the tanks to be given by a parameter alpha. We define the target
region to be one where neither tank is empty and the clock t has reached 3. In Fig. 8
below we show the analysis for an initial region where both reservoirs and both rudder
valves are leaking. The hide statement is a form of existential quantification, allowing
us to solve against the variables of interest. When we run the analysis we obtain the
Analysis Analysis Analysis Analysis AnalysisAnalysisAnalysisAnalysisAnalysis Analysis Analysis Analysis Analysis
Analysis Analysis Analysis Analysis
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[ValveA]=ABNN & loc[GreenRes]=GRL &
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
loc[BlueRes]=BRL
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
reached := reach forward from init_reg endreach;
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
if empty(reached & fin_reg) then
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
prints "Situation is not reachable";
else else else else elseelseelseelseelse else else else else
else else else else
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
print omit all locations hide non_parameters in reached&fin_reg endhide;
Fig. 8. Analysis to derive constraints
following output, which gives the range of values of the parameter and for which the
final region is reachable.
Composing automata *
.Number of iterations required for reachability: 8
Examination of more detailed output shows that the traces requiring the minimal
alpha value of 9/2 are those which involve switching the rudder valve from the primary
to the secondary reservoir at t=1.5, hence for each tank, 3 units are lost from
the reservoir leak, and 1.5 units from the rudder servodyne leaks.
The analysis above involved deriving a constraint on the analog variables of the
system. We could also solve against clock (and other) variables, for example to derive
the maximum time which can elapse before some action must be taken by the user to
preserve system safety. More interestingly, we could extend the user model to include
delays between user observation of some system event, and input of some response by
the user. As mentioned in section 4.2 above, these response times could be based on
empirical data on human performance, allowing us to analyse the system taking into
account the limitations of both the user and the technology.
6.3 Diagnosis activity
Besides finding a fix for a situation in which leaking of hydraulic fluid occurs, the
goal of the pilot is to discover as soon as possible and as precisely as possible which
components in the hydraulics system are leaking. As we have seen in the description of
the case study in section 2 the pilot is supposed to follow a certain diagnosis strategy
in which she switches the valves in different positions and observes the corresponding
changes in the fluid level indicators. In this strategy, the order in which the different
positions of the switches are examined is important because this may influence the
inferences about the status of the system components that the pilot can make in each
step of the diagnosis. Moreover, the pilot has to remember the observations made in
previous steps of the process, in order to reach a complete assessment of component
failures at the end of the diagnosis.
A first analysis that seems useful is to check whether the diagnosis strategy proposed
works for particular 'leaky' situations. This could be done in several ways. One
straightforward way would be to model the diagnosis behaviour of the user as an au-
tomaton. Given the number of possible situations, user observations and inferences that
can be made, this approach seems rather cumbersome and unlikely to scale up when
more difficult cases would be analysed.
A more indirect, but simpler, way to reach the same goal is to use the reachability
analysis language of HyTech. This is the approach we follow in this article.
We start the analysis from a region that characterises the situation in which the
user has switched the valves of the rudder and aileron both to the blue reservoir (i.e.
loc[User]=RBAB). In this situation the user observes a decrease in the blue reservoir
fluid quantity and no decrease in the green reservoir fluid quantity.
Let us assume that the pilot follows the diagnosis strategy indicated in table 1, going
through the various settings from top to bottom. The first situation of the diagnosis can
then be defined as:
By forward reachability we can compute all states that are reachable from this first
situation.
reach forward from sit1 endreach;
We are now interested in those reachable states that correspond to the second situation
in which the user has switched both the rudder and the aileron to green and
observes a decrease in the green fluid but not in the blue while the two reservoirs are
still not empty. The second situation can be characterised as:
We perform a second reachability analysis starting from the intersection of the states
reached in the first analysis s1 and the second situation sit2.
reach forward from s1 & sit2 endreach;
Region s2 in its turn can be intersected with the region describing the next situation
the user may encounter when she switches the aileron back to blue and observes that
both the fluids stopped decreasing. Note that this step corresponds to going from step 2
to step 4 in the diagnosis steps reported in Table 1, skipping the third step listed there.
The resulting regions printed by HyTech of for example s1 & sit2 and s2 & sit3
gives us an indication of the size and complexity of the resulting regions. The resulting
region of s2 & sit3 contains only one element:
This gives exactly one possibility for the locations of the automata as the result
of the diagnosis followed by the user. This unique result indicates that the pilot can
reach only one conclusion about the status of the components of the hydraulics system,
assuming she does not make a mistake in reasoning of course. The conclusion in this
case is that the primary servodyne of the rudder is leaking, but the secondary is not
(RGLN), the green reservoir is not leaking (GRNL), the blue reservoir is not leaking
(BRNL) and the primary servodyne of the aileron is not leaking, but the secondary is
(ABNL). This result corresponds to the combination of the derivations following steps

Table

1.
Note that for this diagnosis we have not made any assumptions about the possibility
that hydraulic components may start leaking while the pilot is performing the diagnosis.
The above analysis shows that in that particular diagnosis, with the described observations
by the pilot, a precise and unique assessment of the status of the hydraulic components
can be reached without excluding in advance that no component starts leaking
during the diagnosis.
It is also interesting to take a look at the region s1 & sit2 that gives the states
that can be reached right after the second observation (step 2) by the pilot. It gives
possible combinations of locations. From the detailed output we can derive what the
pilot could have correctly concluded about the status of the components after the second
step in the diagnosis. The detailed results show that the pilot can correctly conclude
that the blue reservoir is not leaking (BRNL in each possible location vector). But, for
example, the pilot can no longer be sure that the green reservoir is not leaking, although
he could conclude this correctly after the first observation. This is explained by the fact
that the full result obtained from HyTech also takes into account that the green reservoir
could have started leaking during the diagnosis.
If we assume that this is not the case, as the pilot is likely to do in order to reduce
the number of possibilities he has to remember, the number of combinations is reduced
to 9. They are given below without the corresponding constraints on the analog vari-
ables. The result now coincides with the derivations reported in [10] (and table 1), in
which it is stated that the pilot can conclude at this point that at least one of the primary
servodynes is leaking and one of the secondary servodynes, i.e. in none of the
locations the combinations RGN* and AGN* or RG*N and AG*N occurs, where *
stands for N or L. The result can be obtained automatically by adding as an extra constraint
to sit2 the assumption of the pilot that the green reservoir is still not leaking
(loc[GreenRes]=GRNL). This is also one way to make underlying assumptions
concerning the validity of the diagnosis strategy explicit.
The above shows that with the support of HyTech complex situations can be anal-
ysed, that would be difficult to perform accurately by pencil and paper. The analysis of
diagnosis methods can be performed more systematically and thoroughly.
7 Summary and Discussion

Summary

Starting from our concerns with the specification and analysis of interactive systems
with a continuous or hybrid aspect, we have shown that hybrid automata provide a
useful approach to modelling interactive systems with a real-time or continuous aspect.
We believe that if the models so constructed are to be useful as a basis for usability
reasoning, then they must include user relevant abstractions, and if we are to reason
about the operation of the system within a certain context, also environmental aspects
must be considered. Hence in the approach we have taken, we have modelled both
system and user as automata, with links between them via synchronised transitions and
shared variables.
Once the models are constructed, a number of forms of analysis are possible; not
only traditional reachability properties can be examined, such as those pertaining to
safety, but also constraints on the variables of the system can be automatically derived,
such as time constraints. These forms of analysis are similar to those commonly carried
out in the verification of critical systems, albeit with a more explicit human factors
dimension. Task driven analysis, such as the analysis of inferences involved in human
performed diagnosis of system faults, has long been established in the field of human
computer interaction (see for example [5]). However, the approach to the formal support
of such analysis in the context of critical systems which we have presented is a new
application of hybrid automata.
Discussion
Diagnosing failure in process control settings is an important and critical activity in
which the operator of the system is responsible for the safe operation of the system.
Careful design and analysis of diagnosis strategies is therefore very important. The
diagnosis of failures can often not be left completely to a computer system, for example
due to limitations in sensing and monitoring devices [10].
There are a number of interesting possibilities for further work; consider for example
the issue of context. Contextual assumptions can be specified as automata, just
as environmental factors. In [10] for example, it is assumed that no new leaks occur
during the diagnosis. If we label all 'new leak' transitions with a synchronisation label
(eg. start leak), and construct an automaton (Assumption in Fig. 9) with a reflexive
transition in the initial state which synchronises on this label, and a transition to
another state which does not synchronise on the label (NoMoreLeaks in the figure),
then by adding the conjunct loc[Assumption] = NoMoreLeaks to our analysis
regions, we preclude the occurrence of new leaks during the diagnosis.
Assumption Assumption Assumption Assumption AssumptionAssumptionAssumptionAssumptionAssumption Assumption Assumption Assumption Assumption
Assumption Assumption
Assumption Assumption
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Start: True
Leak Leak Leak Leak LeakLeakLeakLeakLeak Leak Leak Leak Leak Leak
Leak Leak Leak NoMoreLeaks NoMoreLeaks NoMoreLeaks NoMoreLeaks NoMoreLeaksNoMoreLeaksNoMoreLeaksNoMoreLeaksNoMoreLeaks NoMoreLeaks NoMoreLeaks NoMoreLeaks NoMoreLeaks
NoMoreLeaks NoMoreLeaks NoMoreLeaks NoMoreLeaks
start_leak start_leak start_leak start_leak start_leakstart_leakstart_leakstart_leakstart_leak start_leak start_leak start_leak start_leak start_leak start_leak
start_leak start_leak
Fig. 9. Assumption automaton
We see this issue of making explicit any assumptions about the context of an anal-
ysis, whether it concerns environmental factors, the operational context (for example
standard operating procedures), or the capabilities and performance limits of the user,
to be a significant benefit of the type of formalisation and analysis described here. At a
practical level, assumptions in this form can be easily added and removed which makes
it easy to perform analysis of the complete system under various assumptions.
Our modelling of the user has been rather simple so far; another interesting area to
explore would be the derivation of more realistic user models, particularly with a psychological
or ergonomic justification, for example modelling user observation, thinking
and reaction times. Toolkits of certain common user behaviours (eg. observation based
on polling) are also an interesting possibility.



--R

Specification and verification of media constraints using uppaal.
Formally verifying interactive systems: A review.
The tool KRONOS.
Using executable interactor specifications to explore the impact of operator interaction error.
Task Analysis for Human-Computer Interaction
Formal Methods for Interactive Systems.
Reasoning about gestural interaction.

Syndetic modelling.
Device models.
Inference and information resources: A design case study.
The theory of hybrid automata.
A model checker for hybrid systems.
Using Autograph to Create Input for Hytech
UPPAAL in a nutshell.

Oops, it didn't arm - a case study of two automation surprises
Using model checking to help discover mode confusions and other automation surprises.
The hybrid world of virtual environments.
--TR
The tool KRONOS
Task Analysis for Human-Computer Interaction
A Review of Formalisms for Describing Interactive Behaviour
HYTECH
The theory of hybrid automata
critical systems;hybrid automata;human factors