Abstract
Formal methods give us techniques to specify the functionality of a system, to verify its correctness or to develop the system stepwise from an abstract specification to its implementation. These aspects are important when designing safety-critical systems. Safety analysis is a vital 1 part of the development of such systems. However, formal methods seldom interface well with the more informal techniques developed for safety analysis. Action systems is a formal approach to distributed computing that has proven its worth in the design of safety-critical systems. The approach is based on a firm mathematical foundation within which the reasoning about the correctness and behaviour of the system under development is carried out. The purpose of this paper is to show how we can incorporate the results of safety analysis into an action system specification by encoding this information via available composition operators for action systems in order to specify robust and safe controllers.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. J. R. Back and K. Sere. From modular systems to action systems. Proc. of Formal Methods Europe’94, Spain, October 1994. Lecture Notes in Computer Science. Springer-Verlag, 1994.
R. J. R. Back and J. von Wright. Trace Refinement of Action Systems. In Proc. of CONCUR-94, Sweden, August 1994. Lecture Notes in Computer Science. Springer-Verlag, 1994.
M. Butler, E. Sekerinski, and K. Sere. An Action System Approach to the Steam Boiler Problem. In Jean-Raymond Abrial, Egon Borger and Hans Langmaack, editors, Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science Vol. 1165. Springer-Verlag, 1996.
E.W. Dijkstra. A Discipline of Programming. Prentice Hall International, Englewood Cliffs, N.J., 1976.
K.M. Hansen, A. P. Ravn and V. Stavridou. From Safety Analysis to Software Requirements. In IEEE Transactions on Software Engineering, Vol.24, No.7, July 1998
N.G. Leveson. Safeware: System Safety and Computers, Addison-Wesley, 1995.
N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese. Requirements Specification for Process-Control Systems. In IEEE Transactions on Software Engineering, 1994.
Z. Liu and M. Joseph. Transformations of programs for fault-tolerance. In Formal Aspects of Computing, Vol 4, No. 5 1992, pp. 442–469
A. McIver, C.C. Morgan and E. Troubitsyna. The probabilistic steam boiler: a case study in probabilistic data refinement. In Proc. of IRW/FMP’98, Australia, 1998.
E. Sekerinski and K. Sere (Eds.). Program Development by Refinement-Case Studies Using the B Method. Springer Verlag 1998.
E. Sekerinski and K. Sere. A Theory of Prioritizing Composition. The Computer Journal, VOL.39, No 8, pp. 701–712. The British Computer Society. Oxford University Press.
K. Sere and E. Troubitsyna. Hazard Analysis in Formal Specification. In Proc. of SAFECOMP’99, France, 1999. To appear.
N. Storey. Safety-critical computer systems. Addison-Wesley, 1996.
E. Troubitsyna. Refining for Safety. TUCS Technical Report No.237, February 1999.
E. Troubitsyna. Specifying Safety-Related Hazards Formally. In Proc. of ISSC’99, USA, 1999. To appear.
K. Wong and J. Joyce. Refinement of Safety-Related Hazards into Verifiable Code Assertions. in Proceedings of SAFECOMP’98,, Heidelberg, Germany, October, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sere, K., Troubitsyna, E. (1999). Safety analysis in formal specication. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_33
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive