Software Engineering - Old Questions

6. Why formal specification is important for software development? Explain.

6 marks | Asked in 2074

formal software specification is a statement expressed in a language whose vocabulary, syntax, and semantics are formally defined. It is a technique for unambiguous specification of software to be build. The specification languages cannot be based on natural language; it must be based on mathematics because natural language specification are informal and usually contain ambiguities.

Fig: Formal specification in software process

The system requirements and system design are expressed in details and carefully analyzed and checked before implementation begins. A formal specification of software is developed after the system requirement have been specified but before the detailed system design. The main benefit of formal specification is its ability to uncover problem and ambiguities in the requirements specification. It forces to system analysis to remove errors and inconsistencies in the requirement specification.

Formal methods are intended to systematize and introduce rigor into all the phases of software development. This helps us to avoid overlooking critical issues, provides a standard means to record various assumptions and decisions, and forms a basis for consistency among many related activities. By providing precise and unambiguous description mechanisms, formal methods facilitate the understanding required to coalesce the various phases of software development into a successful endeavor.

Two fundamental techniques for formal specification are:

1. Algebraic Approach: In algebraic approach, system is described in terms operation and their relationship. It consists of two parts: signature, which determines syntax of operation and an equation, which defines the semantics of operations.

2. Model-Based Approach: In model based approach, the abstract model of system is built using mathematical construct such as set theory, function theory and logic. It specifies the operations performed on abstract model.