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
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.
- [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.
Overview of the Proof Verifier
by C.Pulley. DTI/SERC "SSI Tools" Project, 1995, Nos.7.6
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
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.
- 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
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
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
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
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.
Analysis of the use of Galois Theory to reduce Time/Space Complexities
by C.Pulley. DTI/SERC "SSI Tools" Project, 1994, Nos. U013
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.
- 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.