Application name:

Ammunition Control System

Organisation:

UK Ministry of Defence; Department of Computer Science, Royal Holloway; University of London.

Method:

VDM-SL

Tools:

Specbox and The IFAD VDM-SL toolbox.

Domain:

Miscellaneous

Period:

1990 - 1991

Size:

Roughly 700 lines VDM-SL

Description:

Specification of safety requirements of the explosives storage system (essentially a database) in VDM-SL. Specification was validated by syntax and type checking, and by proving some validation conjectures. Proofs were conducted by hand. Animation was not performed as test data was not available, though an executable model was constructed (in OBJ3).

Conclusions:

Specification exercise highlighted some errors and ambiguities in the English language requirements, so was worthwhile just for that. The unavailability of test data was dissappointing.

Publications:

"The Formal Specification of Safety Requirements for Storing Explosives". P. Mukherjee and V. Stavridou. Formal Aspects of Computing 5(4):299-336, 1993.

Contact:

Name:	Paul Mukherjee
Organisation:	School of Computer Studies
Address:	University of Leeds, Leeds LS2 9JT
Country:	United Kingdom
Phone number:	+44 (113) 2335193
E-mail:	paulm@scs.leeds.ac.uk
Personal website:	http://www.scs.leeds.ac.uk/paulm/

URL:

-

Remarks:

-

© copyright 2004 | Formal Methods Europe