Software Engineering - Old Questions

6.Why do we need formal specification? Discuss behavioral specification in detail.

6 marks | Asked in 2071

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.

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.


Behavioral specification

The simple algebraic technique can be used to describe interfaces where the object state changing depending on the previous operation result. Where this condition holds we say it the behavior properties of system. The specification which is used to specify such type of system property is called behavioral specification.

The object state of the subsystem changes on the result of operations in the object or while interacting with other sub-system objects. The changes of the state of object is called behavioral characteristics of the system. The behavioral state of the formal specification is represented by model-based approach and is expressed as a state model.

Basic types of behavioral specification:

1. Abstract model specifications: defines operations in terms of well-defined mathematical model.

2. Algebraic specifications: defines operations by a collection of equivalence relations.

3. State transition specification: defines operations in terms of states and transitions.

4. Axiomatic specifications: defines operations by logical assertions.