=Paper=
{{Paper
|id=None
|storemode=property
|title=Formal Specification for Design Diversity: Two Case Histories, One Approach
|pdfUrl=https://ceur-ws.org/Vol-639/041-minkowitz.pdf
|volume=Vol-639
|dblpUrl=https://dblp.org/rec/conf/adbis/Minkowitz10
}}
==Formal Specification for Design Diversity: Two Case Histories, One Approach==
https://ceur-ws.org/Vol-639/041-minkowitz.pdf
Formal Specification for Design Diversity:
Two Case Histories, One Approach
Cydney Minkowitz
ALSTOM FERROVIARIA S.p.A., Information Solutions
Via Corticella 75, Bologna, 40128 Italy
cydney.minkowitz@transport.alstom.com
Abstract. Diverse programming is a recommended approach in the preparation
of logic used to drive railway control systems, whereby different
representations and processes are used to configure and validate the logic. This
paper describes how two formal specifications have been used for the
construction of a precise model of the logic, alternative to those represented
using the user and machine notations, and for the construction of software tools
to process the logic, following a rigorous refinement approach. The first
specification was used to develop a redundant tool to check the results of a
logic generator. The second specification was used to verify a logic compiler,
both as an abstract representation, to compare against the compiled code, and as
the design of a diverse code checker.
Keywords: railway interlocking systems, safety-related software, diversity,
model-based formal methods, VDM++
1 Introduction
The Alstom Transport group supplies a family of interlocking systems, known as
SMARTLOCK. Each interlocking system is a computer based railway signalling
system, whose purpose is to ensure the safe movements of trains. Different hardware
and software solutions have been used for the systems, but each is characterized as
having a central subsystem containing generic software that processes code describing
the interlocking logic for a specific signalling area. The logic for each system is
configured using software tools, also developed by Alstom.
The interlocking logic is represented differently for each system. One system,
referred to hereafter as System A, processes logic expressed as Boolean equations,
which are generated using a rule-based tool, and the logic for another system, referred
to hereafter as System B, takes the form of compiled procedural code.
Safety must be assured on all parts of an interlocking system, including the
interlocking logic. The safety assurance techniques recommended for the fixed parts
of the system are well documented, and the generic software of Systems A and B has
been constructed and safety approved on the basis of such recommendations (e.g. the
System A software has a primary-checker architecture, where a checker module
checks the output of the primary software, and System B uses two-out-of three
42 C. Minkowitz
diverse-modular redundancy, where three software modules check each others’
outputs). With regards to the safety assurance of the configuration data, the past
publications (see [1], for instance) have concentrated on the promotion of appropriate
data representations and configuration management procedures, both of which have
also been employed for SMARTLOCK.
The best practice for the construction of railway control and protection software is
documented in the CENELEC EN 50128 standard [2], which provides guidelines on
the techniques to apply for systems with safety integrity levels (SILs) from 0 to 4, of
which interlocking systems are rated as SIL4 (i.e. the maximum). Amongst others, the
standard highly recommends two techniques for the configurable parts of the SIL4
systems - one is the use of diverse programming, whereby protection against random
and systematic faults is achieved through diverse representations and processes
leading to the same results, and the other is the use of formal methods.
The taxonomy of diversity techniques in [3] includes the following list of
techniques applicable for design diversity, the term used for redundant software
programs that compute the same outputs from the same inputs.
1. Separate (independent) developments,
2. Diverse development team,
3. Diversity in description/programming languages and notations,
4. Diverse development platforms and tools,
5. Diverse development methods,
6. Different expressions of substantially identical requirements,
7. Diverse requirements and specifications,
8. Different required properties implying the same behaviour,
9. Requiring different behaviours from the diverse versions.
In line with these recommendations, a software development approach using the
above techniques has been applied for SMARTLOCK - first to develop a diverse
logic generator for System A applications, and second to verify the logic compiled for
System B applications, both as an abstract representation, to compare against the
compiled code, and as the design of a diverse code checker. In particular, the use of a
formal language as a specification notation, and as the basis of a development
method, has led to alternative models of the interlocking logic and alternative means
of implementing the tools.
Sections 2 and 3 give a description of the interlocking logic used for System A and
System B applications and relate the background that motivated the development of
the two aforementioned configuration tools and the use of the formal specifications.
Following a formal development approach, the specifications were refined into
designs to be implemented directly in code. VDM++ was used as the specification
language, and Common Lisp was used as the programming language. Section 4
discusses the rationale for this choice, with example excerpts of the VDM++
specifications of the two configuration tools, and with an explanation of how the
approach was specifically applied to each tool.
The conclusions in Section 5 present the results accomplished by applying the
approach to the two tools, both in its use as a technique for design diversity and as an
effective software development method in general.
Formal Specification for Design Diversity: Two Case Histories, One Approach 43
2 Diverse Logic Generator
The interlocking logic for a System A application is expressed as a sequence of
Boolean equations. Each equation specifies a relation between Boolean-valued input
variables and output variables. An input variable represents an indication received by
the interlocking from some signalling component, i.e. some mechanism, such as a
relay, used to control or monitor some physical device, such as a signal, set of points
or track circuit. An output variable represents a command sent from the interlocking
to some signalling component. The values of the variables represent the on/off states
of the components. The expression defining the relationship between the inputs and
outputs is written in terms of the logical 'not', 'and' and 'or' operators (expressed using
the symbols “.N.”, “*” and “+”, respectively). Operating in split second cycles, the
System A application continually receives the inputs, processes the Boolean
equations, and transmits the outputs.
For example, Extract 1 contains Boolean equations that define the logic for the
simple interlocking scheme shown in Figure 1, which contains two routes, RR1_4
from location 1 to location 4 in the right direction, and RL4_1 from location 4 to
location 1 in the left direction, where there is one equation for each route.
44
4
1
1
Fig. 1. Example interlocking scheme
BOOL RR1_4_CR =
( RR1_4_LORCV * P1_4_DI * .N.P1_4_PULL_LORCV *
.N.RL4_1_NXC
+ B1_4_PUSH_LORCV * P1_4_DI * .N.B1_4_PULL_LORCV *
.N.RL4_1_NXC )
BOOL RL4_1_NXC =
( RL4_1_LORCV * P4_1_DI * .N.B4_1_PULL_LORCV *
.N.RR1_4_CR
+ B4_1_PUSH_LORCV * P4_1_DI * .N.B4_1_PULL_LORCV *
.N.RR1_4_CR )
Extract 1. Logic expressed as Boolean equations
An alternative way of representing the interlocking logic is to specify the relations
between the inputs and outputs using circuit diagrams. A circuit diagram consists of
one or more terminal components, representing the outputs, and a network of non-
terminal components, representing the inputs, linked together using 'inverse', 'serial'
and 'parallel' connections. Because interlocking technology has its roots in relay
technology, signalling engineers traditionally use circuit diagrams to design the
44 C. Minkowitz
interlocking logic. Being equivalent representations, it is possible to convert the
circuit diagrams to their Boolean equation counterparts. For example, the two circuit
diagrams in Figure 2, containing terminal components for setting the routes, and
containing non-terminal components to detect whether the routes are requested (via
the energised contacts “RR1_4” and “RL4_1”), the points on the routes are controlled
in the correct position (via the energised contacts “P1_4” and “P4_1”), the devices
used to request the routes are in the correct states (via the buttons “B1_4” and
“B4_1”) and the opposing routes are not set (via the de-energised contacts “RL4_1”
and “RR1_4”), are an equivalent description of the Boolean equations in Extract 1.
+24 V P1_4 +24 V P4_1
RR1_4 RL4_1
B1_4 B4_1
RR1_4 RL4_1
RL4_1 -24 V RR1_4 -24 V
Fig. 2. Logic described as circuit diagram
The circuit diagrams are designed according to signalling principles, which
incorporate safety and logistical constraints that govern how the interlocking must
work for different railway operating companies. Analysis of the signalling principles
has led to the identification of common network compositions, which may be reused
for different interlocking applications, and the construction of schemas (generic
templates and rules) for the design of the interlocking logic. This, in turn, gave rise to
the requirement for a software tool that would generate automatically the interlocking
logic from the schemas.
The design of the logic generator tool was commissioned nearly twenty years ago
to the University of Bologna by the SASIB Railway Group in Bologna (which later
became Alstom Ferroviaria S.p.A.), as part of a research project to investigate the use
of rule-based techniques for interlocking data configuration. An early prototype of the
tool was produced in the late 1980s using Quintus Prolog. The Prolog program was
developed further within the Alstom group in the early 1990s, and has evolved over
time to its current state. The program has been used since on numerous interlocking
applications for different operating companies.
The program inputs files containing a given interlocking logic schema and files
containing Prolog facts denoting the properties and layout of a given signalling area.
The schema is expressed in an Alstom propriety meta-language, based on the Prolog
syntax, which has features resembling a higher-order predicate calculus. As an
example, Extract 2 contains a logic design rule for creating networks used for route
setting, expressed in a simplified variant of the meta-language notation.
The program compiles a knowledge base from the schema and facts, constructs the
logic and outputs the Boolean equations derived by applying the schema to the facts.
Formal Specification for Design Diversity: Two Case Histories, One Approach 45
network_set_route(Dir, StartLoc, EndLoc) <--
exists(route(StartLoc, EndLoc, Dir)) and (
component(relay, route_set(Dir, StartLoc, EndLoc)) or
component(button, route_set(StartLoc, EndLoc)) ) and
network(points_controlled(StartLoc, EndLoc)) and
not component(button, route_cancelled(StartLoc, EndLoc)) and
if(
exists(route(OppStartLoc, OppEndLoc, OppDir)),
opposing_route(StartLoc, EndLoc, OppStartLoc, OppEndLoc) and
not component(relay, set_route(OppDir, OppStartLoc, OppEndLoc)) )
).
Extract 2. Logic design rule in Prolog syntax
Having realized the requirement for the automatic generation of the interlocking
logic, there remained the problem of validating the logic. In the early years, the logic
was validated by manual inspection of the Boolean equations output. This practice,
being time consuming and error prone, could not be sustained in the long term,
especially with the increasing size and complexity of the new interlocking
applications to come, and so new validation approaches were evaluated, and, in 2001,
a decision was made to develop a diverse logic generator. The two tools could then be
executed independently on the same input files, generating two output files which
could be compared automatically by commercial off-the-shelf file comparison tools
(see Figure 3).
Boolean
logic generator equations
file
schema & fact compare
files
Boolean
equations
diverse
file
logic generator
Fig. 3. Logic generation using diverse software
The second tool was to be developed independently from the first tool, using a
different team and alternative techniques and tools. Given that the only
documentation on the first tool, available at the time when the second tool was
conceived, consisted of a user manual and the Prolog program itself, in order to
understand the nature of the schema meta-language and how it was to be interpreted,
it was considered necessary to begin the development with a precise specification
written in a suitable notation, for which VDM++ was chosen.
The main purpose of the specification was to:
construct a model of the circuit diagrams used to describe the interlocking logic;
formalise the conversion rules used to generate Boolean equations from the logic;
construct a model of the schema definitions embodying the templates and rules
used to construct the interlocking logic;
formalise the reasoning mechanisms used to apply the schema to the facts.
46 C. Minkowitz
So as not to be influenced by the design of the first tool, the specification of the
second tool was created from first principles (based on prior knowledge of formal
logic and rule-based systems), using the first tool as a black box in order to analyse
the required behaviour, by observing its results when applied to example scenarios.
Although the formal specification was used initially as an aid to understanding the
requirements, in the end, it served as an alternative representation of the meta-
language. For example, Extract 3 shows how the design rule in Extract 2 is expressed
in VDM.
kb.defineDesignRule(
"network_set_route",
["Dir","StartLoc","EndLoc"],
kb.guardedDesignInstruction(
kb.predicate(
"route",
["StartLoc","EndLoc","Dir"]),
kb.andConstruction(
kb.orConstruction(
kb.componentAssociation(
,
kb.componentFunction(
"route_set",
["Dir","StartLoc","EndLoc"])),
kb.componentAssociation(