References

[1] F. Andersen, K.D. Pertersen, and J.S. Pettersson. Program verification using HOL-UNITY. In Joyce and Seger [50], pages 1--17.

[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.


[Go Up].
Matthew Morley, Edinburgh. Date: 29 November, 1998