Summary
Proving properties of a specification can deepen our knowledge of the specification, leading to clearer specifications, and more elegant and efficient designs. In this chapter we use an existing specification (Mukherjee and Stavridou’s model of UN regulations for safe storage of explosives) to illustrate this idea. In particular we demonstrate how to discharge a satisfiability proof obligation, and how to prove the correctness of a specification modification. We see that both proofs further our understanding of the specification and the system itself.
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.
Similar content being viewed by others
Bibliography
J.C. Bicarregui, J.S. Fitzgerald, P.A. Lindsay, R. Moore, and B. Ritchie. Proof in VDM: A Practitioner’s Guide. Springer-Verlag, 1994.
Committee of Experts on the Transport of Dangerous Goods, New York. Recommendations on the Transport of Dangerous Goods 5th revised edition, 1988.
R. Elmstrpm, P.G. Larsen, and P.B. Lassen. The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications. ACM Sigplan Notices, 29 (9), 1994.
J. S. Fitzgerald. A proof of Satisfiability in Mukherjee and Stavridou’s Ammunition Control System. Technical Report 616, Dept. of Computing Science, University of Newcastle upon Tyne, Newcastle upon Tyne, NE1 7RU, UK, 1997.
J. Goguen and T. Winkler. Introducing OBJ. Technical Report SRI-CSL88–9, SRI International, August 1988.
I. Lakatos. Proofs and Refutations Cambridge University Press, 1976.
P. Mukherjee. Proof of Equivalence in the ACS specification. Technical Report SCS 97.34, University of Leeds, 1997.
P. Mukherjee and V. Stavridou. The Formal Specification of Safety Requirements for Storing Explosives. Formal Aspects of Computing, 5 (4): 299–336, 1993.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag London Limited
About this chapter
Cite this chapter
Mukherjee, P., Fitzgerald, J. (1998). The Ammunition Control System. In: Bicarregui, J.C. (eds) Proof in VDM: Case Studies. Formal Approaches to Computing and Information Technology (FACIT). Springer, London. https://doi.org/10.1007/978-1-4471-1532-8_2
Download citation
DOI: https://doi.org/10.1007/978-1-4471-1532-8_2
Publisher Name: Springer, London
Print ISBN: 978-3-540-76186-0
Online ISBN: 978-1-4471-1532-8
eBook Packages: Springer Book Archive