Abstract
Today the development of safety-critical systems is to a large extent guided by standards that make demands on both development process and system quality. Before the advent of these standards, development was typically done on a “best practise” basis which could differ much between application areas. Some safety-critical systems (e.g. railway interlockings) have a long technical and economical lifetime so that today we have many legacy safety-critical systems in operation which were developed according to practises that would be regarded as unacceptable today. Usually, such systems are allowed to continue operating by virtue of past performance. If there is doubt about the integrity of a legacy system, an alternative to replacement could be making a “retrospective” safety case demonstrating that the legacy system is indeed safe to use. Using as example a case taken from railway signalling, we will show how formal verification can be used in a retrospective safety case. In this application of formal methods several particular problems arise, such as uncertainty about the original requirements and the required safety level of the various system functions. We will discuss such problems and the approach taken to deal with them in the example case.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Åsta-ulykken 4. januar 2000 – Hovedrapport, The Norwegian Ministry of Justice and the Police (2000)
Benveniste, A., Berry, G.: The Synchronous Approach to Reactive and Real- Time Systems. Proceedings of the IEEE 79(9), 1270–1282 (1991)
Clarke, M.E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Eriksson, L.-H.: Formalising Railway Interlocking Requirements, Technical report 1997:3, Swedish National Rail Administration (1997)
Eriksson, L.-H.: Formal Verification of Railway Interlockings, Technical report 1997:4, Swedish National Rail Administration (1997)
Eriksson, L.-H.: Specifying Railway Interlocking Requirements for Practical Use. In: Schoitsch, E. (ed.) Proceedings of the 15th International Conference on Computer Safety, Reliability and Security (SAFECOMP 1996). Springer, Heidelberg (1996)
Eriksson, L.-H., Johansson, K.: Using formal methods for quality assurance of interlocking systems. In: Mellit, B., et al. (eds.) Computers in Railways IV. Computational Mechanics Publications (1998)
Huber, M., King, S.: Towards an Integrated Model Checker for Railway Signalling Data. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 204–223. Springer, Heidelberg (2002)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th ACM/IEEE Design Automation Conference (DAC 2001), pp. 530–535. ACM/IEEE (2001)
Railway Applications: The Specification and Demonstration of Reliability, Availability, Maintainability and Safety (RAMS), European standard EN50126, CENELEC, Brussels (1999)
Railway Applications – Communication, signalling and processing systems – Software for railway control and protection systems, European standard EN50128, CENELEC, Brussels (2001)
Railway Applications – Safety related electronic systems for signalling, European standard ENV50129, CENELEC, Brussels (1998)
Sheeran, M., Stålmarck, G.: A tutorial on stålmarck’s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 82–99. Springer, Heidelberg (1998)
Zhang, H.: SATO: An Efficient Propositional Prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eriksson, LH. (2004). Using Formal Methods in a Retrospective Safety Case. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2004. Lecture Notes in Computer Science, vol 3219. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30138-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-30138-7_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23176-9
Online ISBN: 978-3-540-30138-7
eBook Packages: Springer Book Archive