|
| | | |
Requirements Reformulation using Formal Specification: A Case Study
Wildman, L.
This article describes our experience of using formal specification to reformulate the requirements of the Nulka Electronic Decoy. The Nulka Electronic Decoy is a hovering rocket that lures anti-ship missiles away from the ship. The requirements specification contained informal natural language requirements relating both to time-related performance requirements, and to other physical characteristics that were not time-related. 'Time Interval Calculus' was used for the time-related performance requirements whereas simple mathematics was used for the others, thereby creating two different views of the Decoy. While no conflicting requirements or incorrect values were detected, 50% of the requirements were modified as a result of formalisation and consultation with domain experts. This article describes the techniques that were used, the changes that were made, reflects on lessons learned and discusses related work. |
Cite as: Wildman, L. (2002). Requirements Reformulation using Formal Specification: A Case Study. In Proc. Workshop on Formal Methods Applied to Defence Systems 2002, Adelaide, Australia. CRPIT, 12. Lakos, C., Esser, R., Kristensen, L. M. and Billington, J., Eds. ACS. 75-83. |
(from crpit.com)
(local if available)
|
|