[2]
H.R. Andersen.
Model checking and boolean graphs.
In B. Krieg-Brückner, editor, *Proceedings of the 4th
European Symposium on Programming (ESOP'92)*, volume 582 of *Lecture
Notes in Computer Science*. Springer-Verlag, 1992.

[3]
H.R. Andersen.
*Verification of Temporal Properties of Concurrent Systems*.
PhD thesis, Århus Universitet, 1993.

[4]
W. Atkinson and J. Cunningham.
Proving properties of a safety critical system.
*Software Engineering Journal*, 6(2):41--50, 1991.

[5]
A. Beveniste.
Synchronous languages provide safety in reactive system design.
*Control Engineering*, Sept. 1994.

[6]
G.M. Birtwistle and P.A. Subrahmanyam, editors.
*Current Trends in Hardware Verification and Automated Theorem
Proving*. Springer-Verlag, 1989.
Proceedings of the 1988 Banff Workshop on Hardware Verification.

[7]
T. Bolognesi and E. Brinksma.
Introduction to the ISO specification language LOTOS.
*Computer Networks and ISDN Systems, North-Holland*, 14:25--59,
1987.

[8] A railway signalling case study for FOREST. Internal publication by British Rail Research, London Rd., Derby, England, 1988. Issue B, ELS-DOC-4314.

[9] SSI Data Preparation Guide. Published by British Railways Board, Feb. 1990. ELS-DOC-3080, Issue K of SSI8003-INT and supplements; British Rail Research, London Road, Derby, England.

[10]
J. Bradfield and C. Stirling.
Local model checking for infinite state spaces.
*Theoretical Computer Science*, 96:157--174, 1992.

[11]
J.C. Bradfield.
*Verifying Temporal Properties of Systems with Applications to
Petri Nets*.
PhD thesis, University of Edinburgh, 1991.
Available as CST-83-91.

[12]
R.E. Bryant.
Graph-based algorithms for boolean function manipulation.
*IEEE Transactions on Computers*, C-35(8):677--91, 1986.

[13]
J.R. Burch, E.M. Clark, et al.
Symbolic model checking: 10^20 states and beyond.
In *Proceedings of Fifth Annual IEEE Symposium on Logic in
Computer Science*, pages 428--39. Computer Society Press, 1990.

[14]
J.R. Burch, E.M. Clark, et al.
Symbolic model checking for sequential circuit verification.
*IEEE Transactions on Computer-Aided Design of Integrated
Circuits*, 13(4):401--24, 1994.

[15] J. Camilleri and T. Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory, 1993.

[16]
K.M. Chandy and J. Misra.
**Parallel Program Design: A Foundation**.
Addison-Wesley, 1988.

[17]
A. Church.
A formulation of the simple theory of types.
*Journal of Symbolic Logic*, 5(1):56--68, 1940.

[18]
E.M. Clarke, E.A. Emerson, and A.P. Sistla.
Automatic verification of finite-state concurrent systems using
temporal logic specifications.
*ACM Transactions on Programming Languages and Systems*,
8(2):244--63, 1986.

[19]
R. Cleaveland.
Tableau-based model checking in the modal mu-calculus.
*Acta Informatica*, 27:725--47, 1990.

[20]
R. Cleaveland, J. Parrow, and B. Steffen.
The concurrency workbench: A semantics-based verification tool for
finite-state systems.
In *Proceedings of the 9th IFIP Symposium on Protocol
Specification, Testing and Verification*, pages 287--302. North-Holland,
1989.

[21] G.V. Conroy and C. Pulley. Logical methods in the formal verification of safety-critical software. Presented at the IMA Conference on Dependable Computing, Sept. 1993.

[22]
D. Craigen, S. Gerhart, and T. Ralston.
*An International Survey of Industrial Applications of Formal
Methods---Purpose, Approach, Analysis and Conclusions*, volume 1.
NIST (National Institute of Standards and Technology),
1993.

[23]
D. Craigen, S. Gerhart, and T. Ralston.
*An International Survey of Industrial Applications of Formal
Methods---Case Studies*, volume 2.
NIST (National Institute of Standards and Technology),
1993.

[24]
A.H. Cribbens.
Solid State Interlocking (SSI): an integrated electronic signalling
system for mainline railways.
*Proc. IEE*, 134(3):148--58, 1987.

[25]
A.H. Cribbens and I.H. Mitchell.
The application of advanced computer techniques to the generation and
checking of SSI data.
*Proceedings of the Institute of Railway Signalling Engineers*,
1992.

[26]
W.J. Cullyer and W. Wong.
Application of formal methods to railway signalling---a case study.
*IEE Computing and Control Engineering Journal*, 4(1):15--22,
1993.

[27]
R. de Simone.
Higher-level synchronising devices in Meije-SCCS.
*Theoretical Computer Science*, 37:245--67, 1985.

[28]
E.A. Emerson.
Temporal and modal logic.
In *Handbook of Theoretical Computer Science*
[96], chapter 16.

[29]
E.A. Emerson and C.-L. Lei.
Efficient model checking in fragments of the modal mu-calculus.
In *Proceedings of the 1st Annual IEEE Symposium on Logic in
Computer Science*, pages 267--78. Computer Sociecty Press, 1986.

[30]
R. Enders, T. Filkorn, and D. Tauber.
Generating BDDs for symbolic model checking in CCS.
In *Proceedings of the 3rd Workshop on Computer Aided
Verification*, 1991.

[31]
A. Fantechi, S. Gnesi, and G. Ristori.
Model checking for action-based logics.
*Formal Methods in System Design*, 4:187--203, 1994.

[32]
S. Fisched, A. Scholz, and D. Taubner.
Verification in process algebra of the distributed control of track
vehicles---a case study.
*Formal Methods in System Design*, 4(2):99--122, 1994.

[33]
R. Floyd.
Assigning meanings to programs.
In *Mathematical Aspects of Computer Science*. American
Mathematical Society, 1967.

[34]
M.J.C. Gordon.
HOL: A proof generating system for higher-order logic.
In G.M. Birtwistle and P.A. Subrahmanyam, editors, *VLSI
Specification, Verification and Synthesis*, Kluwer International Series in
Engineering and Computer Science, pages 73--128. Kluwer, Boston, 1988.

[35] M.J.C. Gordon. Mechanizing programming logics in higher-order logic. In Birtwistle and Subrahmanyam [6], pages 387--439.

[36]
M.J.C. Gordon, R. Milner, and C.P. Wadsworth.
*Edinburgh LCF: A Mechanised Logic of Computation*, volume 78
of *Lecture Notes in Computer Science*.
Springer-Verlag, 1979.

[37]
J. Groote, J. Koorn, and S. van Vlijmen.
The safety guaranteeing system at station Hoorn-Kersenboogerd
(extended abstract).
In *Proceedings of the 10th Annual Conference on Computer
Assurance (COMPASS'95)*, pages 57--68, Gaithersburg, Maryland, 1995.

[38]
A. Gupta.
Formal hardware verification methods: A survey.
*Formal Methods in System Design*, 1:151--238, 1992.

[39]
W.A. Halang and B.J. Krämer.
Safety assurance in process control.
*IEEE Software*, pages 61--7, Jan. 1994.

[40]
J. Harrison.
Binary decision diagrams as a HOL derived rule.
*The Computer Journal*, 38(5), 1995.

[41]
M. Hennessey.
**Algebraic Theory of Processes**.
Foundations of Computing. MIT Press, London, 1988.

[42]
M. Hennessy and R. Milner.
On observing nondeterminism and concurrency.
In *Proceedings of the 7th Colloquium on Automata, Languages and
Programming*, volume 85 of *Lecture Notes in Computer Science*, pages
299--309. Springer-Verlag, 1980.

[43]
M. Hennessy and R. Milner.
Algebraic laws for nondeterminism and concurrency.
*Journal of the ACM*, 32(1):137--161, 1985.

[44]
C.A.R. Hoare.
An axiomatic basis for computer programming.
*Communications of the ACM*, 12(10), 1969.

[45]
C.A.R. Hoare.
**Communicating Sequential Processes**.
International Series in Computer Science. Prentice Hall, 1985.

[46] Software for computers in the application of industrial safety-related systems. International Electrotechnical Commission, 1994. IEC Standard 1131, Part 3.

[47] M. Ingleby. A Galois theory of local reasoning in control systems with compositionality. Presented at the IMA Conference on Dependable Computing, Sept. 1993.

[48]
M. Ingleby and I. Mitchell.
Proving safety of a railway signalling system incorporating
geographic data.
In *Proceedings of SAFECOMP'92*, pages 129--134. IFAC, Pergamon
Press, 1992.

[49]
A. Jowett.
**Jowett's Railway Atlas of Great Britain and Ireland**.
Patrick Stephens Ltd. (Haynes), 1989.
ISBN: 1-85260-086-1.

[50]
J. Joyce and C. Seger, editors.
*Higher Order Logic Theorem Proving and its Applications*, volume
780 of *Lecture Notes in Computer Science*. Springer-Verlag, 1994.

[51]
T. King.
Formalising British Rail's signalling rules.
In *Proceedings FME'94: Industrial Benefit of Formal Methods*,
volume 873 of *Lecture Notes in Computer Science*. Springer-Verlag, 1994.

[52]
D. Kozen.
Results on the propositional mu-calculus.
*Theoretical Computer Science*, 27:333--54, 1983.

[53] L. Lamport. The temporal logic of actions. Technical Report 79, Digital Systems Research Center, 1991.

[54]
K.G. Larsen.
Proof systems for satisfiability in Hennessy-Milner logic with
recursion.
*Theoretical Computer Science*, 72:265--88, 1990.

[55]
S. Malik.
Analysis of cyclic combinational circuits.
*IEEE Transactions on Computer-Aided Design of Integrated
Circuits*, 13(7), 1994.

[56] K. Mark Hansen. Formalising railway interlocking systems. Technical report, Department of Computer Science, Technical University of Denmark, July 1994. Presented at the Nordic Seminar on Dependable Computing Systems.

[57]
K.L. McMillan.
*Symbolic Model Checking: An Approach to the State Explosion
Problem*.
PhD thesis, Carnegie Mellon, 1992.

[58] T.F. Melham. Automating recursive type definitions in higher order logic. In Birtwistle and Subrahmanyam [6], pages 341--86. Proceedings of the 1988 Banff Workshop on Hardware Verification.

[59]
R. Milner.
Calculi for synchrony and asynchrony.
*Theoretical Computer Science*, 25:267--310, 1983.

[60]
R. Milner.
The use of machines to assist in rigorous proof.
*Phil. Trans. R. Soc. Lond.*, 312:411--22, 1984.

[61]
R. Milner.
*A Calculus of Communicating Systems*.
Springer-Verlag, 1990.

[62]
R. Milner.
**Communication and Concurrency**.
International Series in Computer Science. Prentice Hall, 1990.

[63]
R. Milner.
Interpreting one concurrent calculus in another.
*Theoretical Computer Science*, 75:3--13, 1990.

[64]
R. Milner.
Operational and algebraic semantics of concurrent processes.
In *Handbook of Theoretical Computer Science*
[96], chapter 19.

[65]
R. Milner and M. Tofte.
Co-induction in relational semantics.
*Theoretical Computer Science*, 87:209--22, 1990.

[66] I.H. Mitchell. Proposal for an SSI data checking tool. Internal publication by British Rail Research, London Rd., Derby. DE2 8YB, June 1990.

[67] I.H. Mitchell, Nov. 1995. Personal communication.

[68] The procurement of safety critical software in defence equipment (Guidance). UK Ministry of Defence, Apr. 1991. (Interim) Defence Standard 00-55, Part 1.

[69] The procurement of safety critical software in defence equipment (Requirements). UK Ministry of Defence, Apr. 1991. (Interim) Defence Standard 00-55, Part 2.

[70] Hazard analysis and safety classification of the computer and programmable electronic system elements of defence equipment. UK Ministry of Defence, Apr. 1991. (Interim) Defence Standard 00-56.

[71]
F. Moller and C. Tofts.
A temporal calculus of communicating systems.
In *Proceedings of CONCUR'90*, volume 458 of *Lecture Notes
in Computer Science*, pages 401--15, 1990.

[72] M.J. Morley. An heuristic approach to state space reduction of communicating parallel systems. Master's thesis, University of Edinburgh, 1989. Summarised in [73].

[73] M.J. Morley. Tactics for state space reduction on the CWB. Technical Report ECS-LFCS-90-109, Laboratory for Foundations of Computer Science, University of Edinburgh, 1990.

[74] M.J. Morley. Modelling British Rail's interlocking logic: Geographic data correctness. Technical Report ECS-LFCS-91-186, Laboratory for Foundations of Computer Science, University of Edinburgh, 1991.

[75] M.J. Morley. Safety in railway signalling data: A behavioural analysis. In Joyce and Seger [50], pages 465--74.

[76]
O.S. Nock.
**Railway Signalling---a treatise on the recent practice of
British Railways**.
Adam and Charles Black, London, 1980.
Prepared under the direction of a committee of the Institution of
Railway Signalling Engineers under the general direction of O. S. Nock.

[77]
S. Owre, J.M. Rushby, and N. Shankar.
PVS: A prototype verification system.
In D. Kapur, editor, *Proceedings of the 11th International
Conference on Automated Deduction*, volume 607 of *Lecture Notes in
Artificial Intelligence*, pages 748--52. Springer-Verlag, 1992.

[78]
D. Park.
Concurrency and automata on infinite sequences.
In *Theoretical Computer Science*, volume 104 of *Lecture
Notes in Computer Science*. Springer-Verlag, 1981.

[79]
L.C. Paulson.
*The Isabelle Reference Manual*.
Computer Laboratory, University of Cambridge, 1993.

[80]
A. Pnueli.
Applications of temporal logic to the specification and verification
of reactive systems: a survey of current trends.
In *Current trends in Concurrency*, volume 224 of *Lecture
Notes in Computer Science*, pages 510--84. Springer-Verlag, 1986.

[81]
V. Pratt.
A decidable mu-calculus.
In *Proceedings of the 22nd Annual IEEE Symposium on Foundations
of Computer Science*, pages 421--427, 1981.

[82]
G.M. Reed and A. Roscoe.
A timed model of communication sequential processes.
In *Proceedings of ICALP'86*, volume 226 of *Lecture Notes in
Computer Science*, pages 314--23. Springer-Verlag, 1986.

[83]
J. Rushby.
Formal methods in the certification of critical systems.
Technical Report CSL-93-7, SRI International, 1993.
Also: NASA CR 4551 *Formal Methods and Digital Systems Validation
for Airborne Systems*.

[84]
B. Sanders.
Eliminating the Substitution Axiom from UNITY logic.
*Formal Aspects of Computing*, 3(2):189--285, 1991.

[85]
R.C. Short.
Software validation for a railway signalling system.
In *Proceedings of SAFECOMP'83*, pages 183--193. IFAC, Pergamon
Press, 1983.

[86] K. Slind. AC unification in hol90. In Joyce and Seger [50], pages 437--49.

[87] G. Stålmarck. A proof theoretic concept of tautological hardness. Incomplete manuscript circulated to interested parties for review., May 1994.

[88]
G. Stålmarck and M. Säflund.
Modelling and verifying systems and software in propositional logic.
In *Proceedings of SAFECOMP'90*, pages 31--6. IFAC, Pergamon
Press, 1990.

[89]
C. Stirling.
Modal and temporal logics for processes.
Technical Report ECS-LFCS-92-221, Laboratory for Foundations of
Computer Science, University of Edinburgh, 1992.
Lecture notes for the *4th European Summer School in Logic,
Language and Information*, University of Essex.

[90]
C. Stirling and D. Walker.
Local model checking in the modal mu-calculus.
In *Proceedings of the International Joint Conference on Theory
and Practice of Software Development (TAPSOFT'89)*, volume 351 of *Lecture Notes in Computer Science*, pages 368--82. Springer-Verlag, 1989.

[91]
C. Stirling and D. Walker.
A general tableau technique for verifying temporal properties of
concurrent programs.
In *Proceedings of the International BCS-FACS Workshop on
Semantics for Concurrency*, Workshops in Computing, pages 1--15, Berlin,
1990. Springer-Verlag.

[92]
D. Syme.
A new interface for HOL - ideas, issues and implementation.
In T.E. Schubert and P.J. Windley, editors, *Higher Order Logic
Theorem Proving and its Applications*, volume 971 of *Lecture Notes in
Computer Science*. Springer-Verlag, 1995.

[93]
R.D. Tennent.
**Semantics of Programming Languages**.
International Series in Computer Science. Prentice Hall
International, 1991.

[94]
L. Thèry, Y. Bertot, and G. Kahn.
Real theorem provers deserve real user interfaces.
In *Proceedings of the fifth ACM SIGSOFT Symposium on Software
Development Environments*, volume 17 of *Software Engineering Notes*,
1992.

[95]
C. Tofts.
*Proof Systems and Pragmatics for Parallel Programming*.
PhD thesis, University of Edinburgh, 1990.

[96]
J. van Leeuwen.
**Handbook ot Theoretical Computer Science**, volume B.
Elsevier, 1990.

[97]
D. Walker.
Automated analysis of mutual exclusion algorithms using CCS.
*Formal Aspects of Computing*, 1:273--92, 1989.

[98]
P.J. Windley.
The `records`

library.
Unpublished, although available on-line., 1993.
http://lal.cs.byu.edu/lal/holdoc/library/records/records.html.

[99]
W. Wong.
*A Formal Theory of Railway Track Networks in Higher-order Logic
and its Applications in Interlocking Design*.
PhD thesis, University of Warwick, 1991.

[100]
W. Wong.
Modelling bit vectors in HOL: the `word`

library.
In Joyce and Seger
[50], pages 371--84.

Matthew Morley, Edinburgh. Date: 29 November, 1998