Requirements reformulation using formal specification: A case study
Luke Wildman · 2002
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. `Timed 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 conicting 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, reects on lessons learned and discusses related work.