The Structure of Specifications

In my last post I wrote about how to write a decent specification on a quite general level. This time, I like to return to the topic, trying to be a bit more specific and tell you something about how we at Prover like to do things. In the Prover Trident Process, the specification of an interlocking is done in four parts: the Object Model, the Generic Design Specification, the Generic Safety Specification and the Generic Test Specification.

Specifying Interlocking Software

What is it one needs to specify when specifying interlocking software? Basically, a specification should answer two questions: what and how. The ‘what’ part should tell you what the interlocking should do. In order words, it should specify expected behaviour. The ‘how’ part should tell how this expected behaviour is to be accomplished.

The ‘What’ part – What the Interlocking should do

Let’s begin by looking at the ‘what’ part. As we already noted, this is to tell us something about the expected behaviour of the interlocking. To put it simply, the interlocking is expected to allow trains to run in a safe way. If we look closer on this simple statement, we see that it actually contains two parts. The interlocking should allow some things (‘trains to run’) while prohibiting other things (‘in a safe way’). In terms of functionality, it thus makes sense to talk about positive functionality, the things allowed, and negative functionality, the things prohibited.

How does one specify positive functionality? This is nothing else than test cases. For example, if a route fulfills all the requirements for locking and clearing the signal at the beginning of the route, then a request of the route should result in the locking of the route and clearing of the signal. All these test cases are collected in the Generic Test Specification.

What about negative functionality, the things prohibited? Since this is supposed to describe things that are never to happen, it is not practically possible to specify these as test cases. Instead, they are to be thought of as requirements. And since they are to ensure safety, they are actually safety requirements. A typical example could be the following: ‘If a route is locked, then all track curcuits that are part of the route should be free of obstacles’. The safety requirements are written down in the Generic Safety Specification.

The ‘How’ part – How the Interlocking is to function

With the Generic Test Specification and the Generic Safety Specification, we now have a complete answer to the ‘what’ part of the interlocking specification. What remains is the ‘how’ part. This is done in the Generic Design Specification. It should tell us how the interlocking is to function; how are routes to be locked, signals cleared, switches thrown and the like. In other words, the Generic Design Specification is an implementation of all the functions that are to be present in the interlocking.

So are we done now? Well, not quite. The Generic Test and Safety Specifications tells us the expected behaviour of the interlocking, whereas the Generic Design Specification gives an implementation of the interlocking. Hence, they all are supposed to refer to the same thing. The question that remains to be answered is how do we ensure that they do that. Consider route locking, for instance. How do we make sure that the route locking in the Generic Test Specification, the Generic Safety Specification and the Generic Design Specification are all the same? This is where the Object Model comes into play.

The Object Model

The Object Model specifies the types of objects that are present in the interlocking. These can be concrete, representing real railyard objects like track curcuits, signals and switches. They can also be abstract, like routes and local release areas. For each object type, the Object Model specifies a number of things. The exact list may vary, but it typically includes inputs (which may be categorized into physical inputs and inputs from office system); important states, like ‘locked’ for routes; and outputs, including physical outputs. The main thing is that the Object Model provides sufficently rich points of reference to the interlocking so that the other specifications can be written without any further data. It specifies the common concepts of the other specifications.

Although I mention the Object Model last, it is actually the part that should be developed first. Then the Generic Design, Test and Safety Specifications can be developed independently and in parallell.