Information Technology Reference
In-Depth Information
are conditional checks over the current and expected status of the controlled
elements.
In order to give a metric to the dimension of the problem in terms of
parameters of the control tables, we define the
size
of a control table as the
couple
, where
m
is maximum number of inter-dependent equations
involved, that means equations that, taken in pairs, have at least one variable
in common, and
n
is the number of inputs of the control table. We consider
only inter-dependent equations because, if there are sets of equations that
are independent, they can be verified separately, and slicing techniques such
as the ones presented in [13] and [14] can be adopted on the model to reduce
the problem size. In our experiments we basically consider control tables that
have been already partitioned into slices (the size value of a control table is
intuitively the one of its maximal slice).
Correctness of control tables depends also on their model of execution by
the interlocking software. In building CIS, the manufacturers adopt the prin-
ciple of
as safe as the relay based equipment
[1], and often the implemented
model of execution is very close to the hardware behaviour. According to the
semantics of the ladder diagrams traditionally used for defining the control
tables, we have chosen a synchronous model with global memory space where
variables are divided into input, output and latch (i.e., local)[4]. The model
of execution is a state machine where equations are executed one after the
other in a cyclic manner and all the variables are set at the beginning of
each cycle and do not change their actual value until the next cycle. This is
a reasonable generic paradigm for centralized control tables.
Timer variables are not considered in our models, since they are normally
related to functional requirements of the system (e.g., the operator shall press
the button for at least 3 seconds to require a route). Safety requirements
such as the ones considered in this study are normally independent from
timers. An intuitive argument in support of the fact that timers are not
used to implement safety functions is that, in traditional RIS, timers were
implemented by means of capacitors: these are components that have a rather
high failure rate, making them unsuitable for safety functions.
We have developed a tool that generates a set of equations coherent with
this model of execution, expressed as models suitable for automatic verifi-
cation with NuSMV (see sect.4) or SPIN (see sect.5), and which represent
typical control tables of parametric size.
(
m, n
)
3
Safety Requirements
Given a control table representation we want to assess that its design is cor-
rect. In the proposed experiment, we need to check that safety properties
are verified, and this represents the worst case for a model checker: explicit
and symbolic model checkers are challenged by verification of safety proper-
ties, since, in order to show their correctness, they have to explore the entire
state space, or its symbolic representation. Safety requirements typical of sig-
