What is Formal Technique in Software Engineering?

Formal Technique in Software Engineering:

A formal technique is a mathematical method to specify a hardware or software system. It verifies whether a specification is realisable, and verifies that an implementation satisfies its specification. It proves the properties of a system without necessarily running the system, etc. The mathematical basis of a formal method is provided by its specification language.

More precisely, a formal specification language consists of two sets —syn and sem, and a relation sat between them. The set syn called the syntactic domain, the set sem called the semantic domain, and the relation sat called the satisfaction relation.

Syntactic domains:

The syntactic domain of a formal specification language consists of an alphabet of symbols and a set of formation rules to construct well-formed formulas from the alphabet. The well-formed formulas used to specify a system.

Semantic domains:

Formal techniques can have considerably different semantic domains. Abstract data type specification languages used to specify algebras, theories, and programs. Programming languages used to specify functions from input to output values.

Satisfaction relation:

Given the model of a system, it is essential to determine whether an element of the semantic domain satisfies the specifications. This satisfaction is determined by using a homomorphism known as the semantic abstraction function. The semantic abstraction function maps the elements of the semantic domain into equivalent classes.

There can be different specifications describing different aspects of a system model, possibly using different specification languages. Some of these specifications describe the system’s behaviour and others describe the system’s structure. Consequently, two broad classes of semantic abstraction functions are defined— those that preserve a system’s behaviour and those that maintain a system’s structure.