In this paper a novel approach to Discrete Events System is introduced. This approach makes use of array-based logic, and shows how it is possible to guarantee a complete and mathematically consistent description of the functionality. A simple example of the communication between a railway central interlocking system and a signal is used to demonstrate this modelling technique.
In spite of the fact that railways have existed for more than 150 years, it is still debated how to establish a fundamental mathematical theory for modelling requirements and building signal interlocking systems. Until now the development has been pragmatic learning by doing. However as the systems are becoming increasingly more complex, various logical-mathematical new approaches have been proposed. One of this approaches, to be discussed in this paper, is array-based logic [Franksen 1978 & 1984, Møller 1995] the use of which for modelling signal interlocking systems has been demonstrated in a earlier paper [Kristensen 1995.2].
To facilitate the discussion we shall consider a simplified but typical situation inspired by a communication problem, in safety critical systems.
A central Signal Interlocking System (SIS) sends orders through a communication network (see Figure 1). Some of the orders will go to the signal in order to set the signal on green (Go) or on red (Stop). Associated with the signal there is a Discrete Event System (DES), that turns the appropriate lamps on or off depending upon the last input from the SIS. There is however one critical problem of any such system implementation. That is, if the signal shows Go and the communication network breaks down, then the signal will continue to show Go, independent of whether or not a train passes the signal. This will cause a critical situation. To avoid this, the signal will go to its safe state Stop, if not updated every half second.
In the following we will demonstrate how array-based logic can be used to design a discrete event system, that will satisfy all the requirements stipulated for such a situation. To keep the discussion simple and focus on the array-based techniques, we shall confine ourselves to the basic functionality of such a system.
In the state Stop the signal shows stop and, similarly, in the state Go, the signal shows go. The state transition in this graph can be represented by a so-called precedence matrix defined by these two states on each of the two axes, called CurrentState and NextState respectively, as shown in Figure 3. This gives a 2-by-2 full unit matrix, since it is possible to go from any state to any state including itself. From a logically point of view this is a tautology.
Each of the elements in this matrix represents a state transition, but it does not describe anything about the constraints associated with such a transition. Therefore, we will now substitute each of the elements by an array representing the constraints for that particular transition. For example, to change the signal from Stop to Go, the SIS sends the order Go (see Figure 4). If no order Go is received, the transition must not occur, regardless of whether the SIS sends Stop or NoOrder. This explains the only 1 (valid solution) and the two 0’s (non-valid solution) in the array (see Figure 5). So we add this feature to the graph and the precedence matrix, turning the latter into a nested array. That is, the top level of the nested array is the precedence matrix and the level immediately below this the inputs (i.e., Stop, Go, or NoOrder).
The next constraint we would like to introduce, concerns the state transition from Go to Stop, as shown in Figure 6. This transition will occur either when the system receives a Stop from the SIS or a time-out occurs (TimeOut is true). This gives the 2-by-3 array in Figure 7, where we have all 1’s in the row where TimeOut is true (1), and the same goes for the column where SIS is Stop.
In the graph of Figure 8 we have introduced the last two constraints, namely the state transition from Stop to itself and from Go to itself. This corresponds to diagonal elements in the precedence matrix, which are introduced in Figure 9.
However, we are not finished, because the DES has to restart the timer, whenever it goes into the state Go (see Figure 10). That is, it has to generate an output to the timer whenever the SIS sends a Go (see Figure 11).
To achieve flexibility, the question of invariance is crucial, because it guarantees the preservation of all properties under permutation of the axes over levels. The importance of this is that all calculations of NextState and the corresponding outputs are reduced to a simple table lookup in the run-time environment. To achieve this we must first make the array conform in the sense that all items on top level have the same shape. Thus if we are able to enforce conformity we are guaranteed invariance under nesting [Franksen 1984].
The manner in which we enforce conformity is simply by adding axes to each of the four elements, so that they all hold the same set of axes immediately below the top level. To take the first element, we see that it only holds the axis of SIS, but lacks the two axes TimeOut and TimerRestart (see Figure 11). The interpretation of this lack of axes, is that there are no constraints between the variables defining this pair of axes and the existing SIS axis. In a physical sense this means we have a don’t care situation, which logically is represented by a tautology between the pair of the axes TimeOut and TimerRestart. In other words, this pair of axes spans a table of all 1’s (see Figure 12). To obtain all combinations of this table and the SIS axis, we must introduce their outer product defined in terms of conjunction (and) (see Figure 13).
This approach is repeated for the other three elements resulting in the conforming array of Figure 14. Due to the size of the Figure, the indices are not shown.
The array in this figure is a complete mathematical model of the system, in which all possible combinations are described either as valid 1 or non-valid 0. During this process of making the array conform, we have only introduced tautologies, which makes the logical interpretation of this array mathematically consistent with the original array in Figure 11.
We are now able to permute the axes over the levels of nesting in order to obtain the most convenient representation for table lookup, namely that which mathematically corresponds to indexing of the array. The basic idea is to collect all inputs on one level and all outputs on the other level. We therefore have a choice. For the purpose of illustration, we choose to place all inputs on the top level and all outputs on the level below. This permutation of the axes over the two levels is shown in Figure 15.
As a result the determination of a state is now done by indexing on the top level, since a state is defined by an input. The outcome is a boolean array of outputs on that level. To illustrate, the current state is Go and SIS send the order Go and there is no time-out. That is, the indices are: CurrentState=1, SIS=1 and TimeOut=0 in 0-origin. The resulting array is shown in figure 16.
In this case we see that there is only one valid solution, namely the one where NextState is 1 (Go) and TimerRestart is 1 (true). This means that the next state will be Go and the timer should be restarted.
A more complicated result is obtained, if we change the value of TimeOut to true (1) and maintain the values of the other indices. This is shown in Figure 17.
As a result of this “table-lookup” there are three ways to assign the outputs. In other words the result is non-deterministic. Let us now interpret the boolean value true as the arithmetic value 1 and similarly false as the value 0. With this interpretation we can sum each of the sub-arrays. In this way we obtain the number of ways of assigning the outputs for each of the inputs (see Figure 18).
This result suggests, that the elements can be divided into three groups, according to the number of ways to assign the output. Let us consider these possibilities one by one. If there is one and only one possibility then the outputs it is deterministic. If two, three or more possibilities, it is non-deterministic. Finally, but not illustrated in this example, if there is only zero possibility, no output exists for that particular input.
If the requirement for the system is, that it must be deterministic, we have to rewrite the array so that each of the sub-arrays holds only one value true (1) and the remainder false (0). This can be done either by manipulating the conforming array or by redesigning the constraints in the beginning of the process. It is an obvious requirement that the system must have at least one valid output for each input. Accordingly, if any of the sub-arrays sums to zero, the corresponding constraints must be changed. Alternatively, it must be verified that that particular input will never occur.
Whenever such a system is designed, it is according to a specification of requirements. By means of array-based logic it can be completely verified that the system satisfies these requirements.
For example, a requirement could be: “If the signal is Stop and it receives an order Go from the SIS, then the state should change to Go and the timer should be restarted”. A more formal way to express this:
State=Stop and SIS=Go :: State=Go and RestartTimer
Here the ‘::’ is interpreted as an assignment. In other words, when the left hand side is true, then the variables on the right hand side should be assigned to make the expression true. If the left hand side is false the result on the right hand side is a don’t care situation. These relation between the two sides is shown in Figure 19. That is readily recognised as the truth-table definition of logical implication (denoted: ‘->’ ).
The expressions on either side of the ‘::’ contain a variable called state, representing the state of the DES, but at different times. The state on the left hand side is the current state (CurrentState) and the state on the right hand side is the next state (NextState). Therefore, the expression above denoting Req1, we can rewrite.
Req1: CurrentState=Stop and SIS=Go -> NextState=Go and RestartTimer
This expression can be represented by an boolean array of four axis [Møller 1995], if we define the variables as follows:
CurrentState›'Stop' 'Go'
NextState›'Stop' 'Go'
SIS›'Stop' 'Go' 'NoOrder'
RestartTimer›0 1
The outer product of all four axis gives the entire state-space. Thus according to the specified requirement, the relation between the four axes will be as follows:
Req1 ((CurrentState¨›'Stop')°.^(SIS¨›'Go'))°.ˆ
((NextState¨›'Go')°.^RestartTimer)
This gives the array in Figure 20
This array represents the relation between four variables, which must hold at all time. In other word, if a combination of variables is false (0), then the combination must not be true (1) in the array representing the system. (see Figure 15). To make a complete verification we must take each of the states in the array of Figure 15 and compare it with the array representing the requirement (see Figure 20). The easiest way to do this is by permutation of the axes of array in Figure 15, so the arrays has the same axes at the top level, as shown in Figure 21, we now have four axes SIS, CurrentState, NextState (NS), and TimerRestart (TR) at the top level.
The only axis TimeOut (TO) which is not included in the requirement, is placed immediately below the top level. The top level of the array has the same shape as the array for the requirement and each of the sub-arrays contain the axis that is not present in the requirement. The lack of a variable from the requirement, means that the value of that particular variable is not related to requirement. In the present case the requirement does not specify anything about the time-out, for which reason the TimeOut axis (TO) in Figure 21 must be eliminated. This elimination means that the axis is now a tautology. Since we have reduced the axis by disjunction (or) (in APL:Ÿ/¨).
To demonstrate that the requirement holds for the entire system, the valid solutions in the reduced system array (Figure 22) should be a subset of the valid solutions in the requirement (see Figure 20). More precisely, if a combination of assigning values are valid it should also be valid in the requirement. If it is not valid in this sense, then the system does not satisfy the requirement. This means that in Reduced System Array (RSA) in Figure 22 should imply Req1 element by element.
RSA ˆ Req1
This is verified in Figure 23. Namely all elements are true (1), meaning that the requirement Req1 holds for all possible inputs.
Array-based logic has been developed since 1977 by the Systems Science Group at the Electric Power Engineering Department, Technical University of Denmark, in co-operation with Danish industry. The theoretical representation which have been used in this paper, is however only feasible for small-scale problems because of the excessive demand for computer memory. For example, a small railway station could easily involve in the order of four hundred binary variables corresponding to a system array of 2400 elements [Kristensen 1995.1]. On the other hand, since the number of valid solutions are relatively few, an isomorphic and very compact representation [Møller 1995] has been developed, which have proved itself to be very efficient in modelling large scale systems, in industrial practice.
Array-based logic has proven to be a promising way to designing industrial systems, also outside the railway industry and discrete event systems, because it provides complete and mathematical consistent way of determining all system properties. A engineering platform based on this compact representation is currently being developed in an EUREKA project jointly between Bang & Olufsen, and the Swedish electric power supply company, Sydkraft, in co-operation with the Systems Science Group. A prototype for this new platform is implemented as an auxiliary processor in Dyalog APL.
To explore the possibilities of using this platform for the solution of signal interlocking systems, the Danish State Railways initiated a research project jointly with the Systems Science Group in February 1995 to be concluded in the spring of 1998. The results presented in this paper is a part of this project.
Bo Grave (Kristensen)
Danish State Railway Consult
Signalling Assessment Department
Address: Soelvgade 40, F4
DK-1349 Copenhagen K
Denmark