May 1992 to May 1995

Department of Computation, University of Manchester Institute for Science and Technology

Full-time Research Associate

Employed under the SERC/DTI Advanced Technology Program Safety Critical Systems Initiative (project nos. IED4/1/9035). This was a collaborative project between UMIST, GEC Alsthom Signalling Limited and Westinghouse Signals Limited into the formal analysis and verification of the Solid State Interlocking (SSI) data language (used to specify the functionality of railway signalling interlocking installations).

Inference procedures for verifying behavioural properties of an SSI were specified in Z and implemented in Prolog++.

EPSRC reported that this project had made a very significant contribution to its field.

Research Supervision

Paul Dongha - PhD using resource bounded agents to build formal micro-economic models with temporal/action logics

Papers

Logical Methods in the Formal Verfication of Safety-Critical Software

by C.Pulley and G.V.Conroy. In the IMA Conference Proceedings: Mathematics of Dependable Systems, 1st - 3rd September 1993, Royal Holloway, University of London

Abstract

The purpose of the work reported in this paper is to describe a formal procedure by which one may automatically verify the safety of a specific SSI interlocking. Unlike other research work reported on elsewhere (see eg. [Mor93] and [IngMit92]), we shall explicitly model the IFPs polling cycle within the formalism to be presented shortly. This has the added benefit of enabling us to more correctly model the SSIs behavior and to also formally verify the safety of the IFP. Unlike [IngMit92], we are able to express and verify much more general safety properties. Our work also differs from the above in that we have concentrated on trying to improve the efficiency of our decision procedure rather than by concentrating on the modes by which we may verify certain types of safety property.

References:

  • [Mor93]: Morley, M., J. (1991) Modeling British Rail's Interlocking Logic: Geographic Data Correctness. LFCS Report ECS-LFCS-91-186, University of Edingburgh, November 1991.
  • [IngMit92]: Ingleby, M. and Mitchell, I. (1992) Proving Safety of a Railway Signaling System Incorporating Geographic Data. Proceedings SAFECOMP '92, 28th-30th October 1992, Zurich, Switzerland.

Full paper: [PDF]

Reports

Overview of the Proof Verifier

by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.6

Abstract

This document defines (or rather shows how to!) a Floyd-Hoare programming logic for the SSI Data Language. This programming logic may easily (tediously?) be implemented using techniques from type checking.

Specification of the Proof Assistant

by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.4

Abstract

This report provides a full specification in Z of the proof search algorithm.

The reachability algorithm specified in this report has been structured in a manner similar to the structuring of the various graph algorithms found in the works of Hopcroft and Tarjan. This has enabled a much more generic and flexible approach to the algorithms specification to be taken.

References:

  • Hopcroft, J.E. and Tarjan, R.E. (1973) Algorithm 447: Efficient Algorithms for Graph Maninpulation, Communications of the ACM 16(6), 372-378.
  • Tarjan, R.E. (1972) Depth-First Search and Linear Graph Algorithms, SIAM Journal of Computing 1(2), 146-160.

A Proof Calculus for the SSI Geographic Data Language

by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.2

Efficient Inference Techniques for Verifying that an SSI is Safe/Unsafe

by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.1

Description of the Concrete and Abstract Syntax for the SSI Geographic Data Language

by C.Pulley. DTI/SERC "SSI Tools" Project, 1994, Nos.6.1.2

Abstract

This document is essentially three separate documents all combined into one:

  • Firstly, we have an EBNF description of the concrete syntax for the SSI Data Language.
  • This EBNF description is presented alongside with a Z description of the abstract syntax of the SSI Data Language.
  • Finally, in appendix A, we have a prolog implementation of a parser for the SSI Data Language. The parser is written using the DCG grammar rules of prolog and the rules pass back a prolog implementation of the Z abstract syntax tree, having previously taken in a prolog implementation of the EBNF description of the concrete syntax tree.

Partial Semantics for the SSI Data Language

by C.Pulley. DTI/SERC "SSI Tools" Project, 1993, Nos.6.1.1

Abstract

This document, along with deliverables 6.1.2 and 6.1.3, provides a full syntactic and semantic specification (in the Z notation and a BNF like notation) of the SSI data language and the IFP.

Deliverable 6.1.3 provides a specification of the IFP and how it interacts with and uses information within the SSI data files.

This document describes a semantics for the various constructs used within the SSI data files to describe an interlockings functionality.

Semantics for the Interlocking Functional Program

by C.Pulley. DTI/SERC "SSI Tools" Project, 1993, Nos.6.1.3

Abstract

This document, along with deliverables 6.1.1 and 6.1.2, provides a full syntactic and semantic specification (in the Z notation and a BNF like notation) of the SSI data language and the IFP.

Deliverable 6.1.1 provides a specification of the SSI data language constructs that are used within the various SSI data files to specify an interlockings functionality.

This document describes how the IFP interacts with and uses the information within these SSI data files. The concepts of major and minor cycle are introduced to facilitate the description of the IFP.

Approaches for Automated Reasoning with Solid-State Interlockings and their Geographic Data

by C.Pulley. DTI/SERC "SSI Tools" Project, 1992, Nos.5.1

Abstract

This report introduces some logics that we suggest are of use in the formal specification of existing SSI geographic data. We then go on to show that validity for these logics is decidable.

For us this opens up the possibility of being able to automatically verify that properties hold of our SSI geographic data (in particular, we are here interested in the safety properties of a given railway layout).

The logics we propose to use are based on the second-order monadic theory of successor arithmetic.

Discussion Papers

Analysis of the use of Galois Theory to reduce Time/Space Complexities

by C.Pulley. DTI/SERC "SSI Tools" Project, 1994, Nos. U013

Abstract

The purpose of this technical note is to derive an intuitive representation for the clopen subsets of the topologies defined by Ingleby and Mitchell.

In doing this, we are able to show that the galois theory approach of Ingleby and Mitchell simply partitions the SSI data code up into control fragments that have no or little dependance upon each other. Unfortunately, the majority of railway layouts have lots of interactions and so their partitioning algorithm is of little help with the verification of such layouts.

References:

  • Ingleby, M. and Mitchell, I. (1992) Proving Safety of a Railway Signaling System Incorporating Geographic Data. Proceedings SAFECOMP '92, 28th-30th October 1992, Zurich, Switzerland.