Peter Gorm Larsen
Abstract
Abstract
This short communication is a response to [MuS93] investigating their ACS system specification. The main point in this paper is that executing specifications can be used as a feasible way of validating them. It is essential to have tool support which enables one to write a generally not executable specification, and then prototype (parts of) it directly in the specification language, without translating it into some other prototyping language.
- [AEL92] Making Specifications Executable — Using IPTES Meta-IVMicroprocessing and Microprogramming1992351–5521528Google Scholar
- [BFM89] Bloomfield, R., Froome, P. and Monahan, B.: SpecBox: A toolkit for BSI-VDM.SafetyNet, (5):4–7, 1989.Google Scholar
- [HaJ89] Hayes, I.J. and Jones, C.B.: Specifications are not (necessarily) executable.Software Engineering Journal, pages 330–338, November 1989.Google Scholar
- [ISO93] Information Technology Programming Languages — VDM-SL. Technical report, First Committėe Draft Standard: CD 13817-1, November 1993. ISO/IEC JTC1/SC22/WG19 N-20.Google Scholar
- [Las93] IFAD VDM-SL ToolboxFME'93: Industrial-Strength Formal Methods1993Berlin HeidelbergSpringer-Verlag681Google Scholar
- [MuS93] The Formal Specification of Safety Requirements for Storing ExplosivesFormal Aspects of Computing199354299336Google ScholarDigital Library
Index Terms
- Response to “the formal specification of safety requirements for storing explosives”
Recommendations
The formal specification of safety requirements for storing explosives
AbstractIn this paper we consider the current practices involved in the storage of explosive articles and substances. In the spirit of Defence standard 00-55, we formalize the safety requirements of the ACS software which is used to manage certain MOD ...
Informal and Formal Requirements Specification Languages: Bridging the Gap
The differences between informal and formal requirements specification languages are noted, and the issue of bridging the gap between them is discussed. Using structured analysis (SA) and the Vienna development method (VDM) as surrogates for informal ...
Using KIDS as a tool support for VDM
ICSE '96: Proceedings of the 18th international conference on Software engineeringKIDS/VDM is an experimental environment that supports the synthesis of executable prototypes from VDM specifications. The development proceeds as a series of correctness preserving transformations under the strict control of the tool. A by-product of ...
Comments