|
|
|
|
 |
|
|||||||||||||||||||
 |
Application name: Behavioural Analysis of Geographic Data Organisation: University of Edinburgh, British Rail Research Method: Higher Order Logic Tools: HOL90 Domain: Railway Signalling/Data validation Period: June 1990 - December 1992 Size: Circa 1000 lines of Standard ML; 400 lines of bespoke HOL tactics. Description: The problem was to devise a method of validating the Geographic Data used to parameterise each installation of British Rail's Solid State Interlocking with the control logic for the station or yard in question. The validation problem is a matter of deciding whether the data satisfy certain (generic) safety requirements, so the first task was to identify a suitable collection of safety properties. The second task was to devise a formal semantics for the language used to encode the data, and to implement these semantics as a theory in the HOL theorem prover. From this beginning it was possible to derive a program logic and implement proof tools to carry out the invariance proofs entirely automatically. Conclusions: The HOL theorem prover is the ideal vehicle for developing a prototype embedded application of this type since it is an open programming system, allowing one to experiment with the design of the proof tactics and methodology. A drawback is that since HOL is optimised for interactive use there are inefficiencies that impact negatively on the fully automatic mode of usage when one wishes to scale the approach much beyond the current SSI data size (20Kb). Publications: M.J.Morley, Safety in Railway Signalling Data: A Behavioural
Analysis. 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
Contact:
URL: http://www.scs.leeds.ac.uk/mjm/ Remarks: - |
|||||||||||||||||||
 |
||||||||||||||||||||
|
||||||||||||||||||||
© copyright 2004 | Formal Methods Europe |
||||||||||||||||||||
