Capturing complete and accurate requirements by refinement

Complete and accurate functional requirements are the foundation for valid specification refinement and correctness verification of implemented software systems when they are developed with a formal method. However, capturing quality requirements is a difficult task, and there is a lack of well-defined and effective technique that solves the problem as well. We argue that the refinement technique used in conventional formal methods for transforming formal specifications into programs is actually an effective technique for capturing the functional requirements. We define the completeness of formal specifications and explain by examples how it can be achieved.