Abstract
Formal methods are gradually making their way onto the “shop floor” of software engineering. As part of this process, industrial software developers are conducting trials of formal techniques in realistic projects. This paper describes two such studies: one each from the nuclear and aerospace industries. Both projects stressed the importance of formal specification as a modelling tool in the early stages of system development, but they differed in their approaches to specification validation.
The specification styles and validation activities in the two studies will be compared. Finally the conclusions which can be drawn from projects such as these are discussed.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
[ABH+95] D.J. Andrews, H. Bruun, B.S. Hansen, P.G. Larsen, N. Plat, et al. Information Technology — Programming Languages, their environments and system software interfaces — Vienna Development Method-Specification Language Part 1: Base language. ISO, 1995.
[BFL+94] J. C. Bicarregui, J. S. Fitzgerald, P. A. Lindsay, R. Moore, and B. Ritchie. Proof in VDM: A Practitioner's Guide. FACIT. Springer-Verlag, 1994. ISBN 3-540-19813-X.
T. M. Brookes, J. S. Fitzgerald, and P. G. Larsen. Formal and informal specifications of a secure system component: final results in a comparative study. In Proceedings of FME'96, Lecture Notes in Computer Science. Springer-Verlag, 1996.
Robin Bloomfield, Peter Froome, and Brian Monahan. SpecBox: A toolkit for BSI-VDM. SafetyNet, (5):4–7, 1989.
René Elmstrøm, Peter Gorm Larsen, and Poul Bøgh Lassen. The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications. ACM Sigplan Notices, September 1994.
J. S. Fitzgerald and C. B. Jones. Proof in the Validation of a Formal Model of a Tracking System. Technical report, Dept. of Computer Science, University of Manchester, 1996. In preparation.
J. S. Fitzgerald and M. A. Spink. Formal Modelling of a Tracking System for a Nuclear Plant. Technical report, Dept. of Computer Science, University of Manchester, 1996. In preparation.
N. E. Fuchs. Specifications are (preferably) executable. Software Engineering Journal, pages 323–334, September 1992.
I. J. Hayes and C. B. Jones. Specifications are not (necessarily) executable. Software Engineering Journal, pages 330–338, November 1989.
Cliff B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, Englewood Cliffs, New Jersey, second edition, 1990. ISBN 0-13-880733-7.
Peter Gorm Larsen, John S. Fitzgerald, and Tom Brookes. Applying formal specification in industry. IEEE Software, May 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fitzgerald, J.S. (1996). Two industrial trials of formal specification. In: Wirsing, M., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1996. Lecture Notes in Computer Science, vol 1101. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014302
Download citation
DOI: https://doi.org/10.1007/BFb0014302
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61463-0
Online ISBN: 978-3-540-68595-1
eBook Packages: Springer Book Archive