Refinement in Requirements Specification and Analysis: a Case Study
Edwin de Jong,
Jaco van de Pol and
Jozef Hooman
Appeared in: Proceedings 7th IEEE Conference and Workshop on
the Engineering of Computer-Based Systems (ECBS),
pages 290-298, 2000.
ABSTRACT
This paper presents a formal method for requirements specification and analysis.
Using this method some techniques for step-wise refinement are studied.
During the early phases of system development, where the exact requirements
are yet unclear, these techniques allow to write incomplete and global
specifications, which during successive steps can be refined and completed.
At each step the method supports formal analysis of the specification.
In particular two abstraction techniques are studied:
nondeterminism and uninterpreted symbols.
These techniques are explored using a realistic case study,
that was inspired by the specification of an existing naval
command and control system.
Specifications are written and analysed using the language and proof
checker of
PVS.
Postscript