 |
Requirements Reformulation Using Formal Specification: A Case Study
Wildman, Luke (2002-06-01) Requirements Reformulation Using Formal Specification: A Case Study. Technical Report 02-16, Software Verification Research Centre, School of Information Technology, The University of Queensland.
|
|
| |
| Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials) |
| Name |
Description |
MIMEType |
Size |
Downloads |
svrc_02_16.pdf
|
svrc_02_16.pdf |
application/pdf |
187.82KB |
187 |
svrc_02_16.ps
|
svrc_02_16.ps |
application/postscript |
181.54KB |
58 |
| Author(s) |
Wildman, Luke
|
| Title |
Requirements Reformulation Using Formal Specification: A Case Study
|
| School, Department or Centre |
Software Verification Research Centre, School of Information Technology
|
| Institution |
The University of Queensland
|
| Report Number |
Technical Report 02-16
|
| Publication date |
2002-06-01
|
| Subject |
280302 Software Engineering
|
| Abstract/Summary |
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. Our approach was to translate the NL requirements '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 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.
|
| Keyword(s) |
Requirements engineering
formal methods
Timed Interval Calculus
|
| Additional Notes |
Copyright 2002, Australian Computer Society, Inc. This paper appeared at the Workshop on Formal Methods Applied to Defence Systems, Adelaide, Australia, June 2002. Conferences in
Research and Practice in Information Technology, Vol. 12. L.M. Kristensen and J. Billington, Eds. Reproduction for academic, not-for profit purposes permitted provided this text is
included. Later published as Wildman, Luke (2002) "Requirements Reformulation Using Formal Specification: A Case Study" in Charles Lakos, Robet Esser, Lars M. Kristensen and Jonathan
Billington, editors, Proceedings of the Workshop on Formal Methods Applied Defence Systems, Adelaide, Australia, Conferences in Research and Practice in Information Technology, Vol. 12,
pages 75-83, Australian Computer Society.
|
|
|
|
