Abstracts of Signalling Publications

<BODY> <H1>Abstracts of Signalling related Publications</H1> <BLOCKQUOTE><A NAME="FMERAIL-98"><IMG ALT="" SRC="feather.gif" WIDTH="540" HEIGHT="46"></A> <H1><A HREF="FMERAIL-98.ps.gz">Semantics of Geographic Data Languages </A></H1> M.J.Morley <P> (Participants proceedings of the first FMERail Workshop, June 1998. <A HREF="FMERS-98.ps.gz">Slides.</A>) </P> <H1>Abstract:</H1> When one wishes to use formal verification techniques to reason about the behaviour of computer controlled railway signalling systems, particularly if the objective is to check their safety properties, a rigorous mathematical semantics for the language used to program the signalling functions is essential to any meaningful verification strategy. This paper motivates the need for formal semantics in such applications, and illustrates how an operational semantics for the language used to program Railtrack's Solid State Interlocking (SSI) may be defined. </BLOCKQUOTE> <BLOCKQUOTE><A NAME="SCP-97"><IMG ALT="studio433--" SRC="feather.gif" WIDTH="540" HEIGHT="46"></A> <H1><A HREF="SCP-97.ps.gz">Safety-level Communication in Railway Interlockings</A> </H1> M.J.Morley <P> In <EM>Science of Computer Programming</EM>, Vol. 29, Nos. 1-2, July 1997, pp 149-172. </P> <H1>Abstract:</H1> This paper illustrates the formal analysis of a simple protocol to convey critical data between the distributed solid state control elements in the signalling systems operated by Railtrack (British Railways). The analysis concentrates on temporal properties of the protocol, and one safety property in particular which <EM>informal</EM> analysis suggests can be violated in certain combinations of circumstances. A formal model is developed so that a rigorous, mathematically informed, assessment can be made as to whether the perceived violation of safety presents a significant hazard to railway traffic. The model is used to formulate possible strategies to overcome the problem. While demonstrating the power of the modelling process, this paper also illustrates the importance of conducting formal proofs: the failed attempt to prove safety in a corrected version of the protocol reveals a second logical flaw. Both flaws admit simple solutions. </BLOCKQUOTE> <BLOCKQUOTE><A NAME="THESIS"><IMG ALT="studio433--" SRC="feather.gif" WIDTH="540" HEIGHT="46"></A> <H1><A HREF="thesis.html">Safety Assurance in Interlocking Design</A> </H1> M.J.Morley <P> <EM>Safety Assurance in Interlocking Design</EM>. PhD thesis, University of Edinburgh, 1996. </P> <H1>Abstract:</H1> This thesis takes a pedagogical stance in demonstrating how results from theoretical computer science may be applied to yield significant insight into the behaviour of the devices computer systems engineering practice seeks to put in place, and that this is immediately attainable with the present state of the art. The focus for this detailed study is provided by the type of solid state signalling systems currently being deployed throughout mainline British railways. Safety and system reliability concerns dominate in this domain. With such motivation, two issues are tackled: the special problem of software quality assurance in these data-driven control systems, and the broader problem of design dependability. In the former case, the analysis is directed towards proving safety properties of the geographic data which encode the control logic for the railway interlocking; the latter examines the fidelity of the communication protocols upon which the distributed control system depends. <P>The starting point for both avenues of attack is a mathematical model of the interlocking logic that is derived by interpreting the geographic data in process algebra. Thus, the emphasis is on the semantics of the programming language in question, and the kinds of safety properties which can be expressed as invariants of the system's ongoing behaviour. Although the model so derived turns out to be too concrete to be effectual in program verification in general, a careful analysis of the safety proof reveals a simple co-induction argument that leads to a highly efficient proof methodology. From this understanding it is straightforward to mechanise the safety arguments, and a prototype verification system is realised in higher-order logic which uses the proof tactics of the theorem prover to achieve full automation. </P> <P>The other line of inquiry considers whether the integrity of the overall design that coordinates the activities of many concurrent control elements can be compromised. Therefore, the formal model is developed to specifically answer safety-related concerns about the protocol employed to achieve distributed control in the management of larger railway networks. The exercise reveals that moderately serious design flaws do exist, but the real value of the mathematical model is twofold: it makes explicit one's assumptions about the conditions under which the faults can and cannot be activated, and it provides a framework in which to prove a simple modification to the design recovers complete security at negligible cost to performance. </P></BLOCKQUOTE> <BLOCKQUOTE><A NAME="HUG-93"><IMG ALT="studio433--" SRC="feather.gif" WIDTH="540" HEIGHT="46"></A> <H1><A HREF="HUG-93.ps.gz">Safety in Railway Signalling Data: A Behavioural Analysis </A></H1> M.J.Morley <P> In proceedings of the 6th annual Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, 4--6 August, 1993, LNCS Vol. 740, Springer-Verlag </P> <H1>Abstract:</H1> Higher Order Logic is used to analyse safety properties of a computer based railway signal control system. British Rail's Solid State Interlocking is a data driven controller whose behaviour is governed by rules stored in a geographic database. The correctness of these data are highly critical to the system's safe operation. Taking as our starting point Gordon's implementation of program logics in Higher Order Logic, we formalise the data correctness problem in a natural way, designing tactics to automate much of the verification task. Our approach requires quadratic time and linear space, and is thought to be adequate for the current generation of Solid State Interlockings. Properly formalised, the compositional proof strategy we suggest will allow us to scale up our analyses arbitrarily. </BLOCKQUOTE> <HR> <ADDRESS>Matthew Morley, Edinburgh. Date: 29 November, 1998</ADDRESS> </BODY>