by Dinesh Thakur

The formal methods model is concerned with the application of a mathematical technique to design and implement the software. This model lays the foundation for developing a complex system and supporting the program development. The formal methods used during the development process provide a mechanism for eliminating problems, which are difficult to overcome using other software process models. The software engineer creates formal specifications for this model. These methods minimize specification errors and this result in fewer errors when the user begins using the system.

Formal methods comprise formal specification using mathematics to specify the desired properties of the system. Formal specification is expressed in a language whose syntax and semantics are formally defined. This language comprises a syntax that defines specific notation used for specification representation; semantic, which uses objects to describe the system; and a set of relations, which uses rules to indicate the objects for satisfying the specification.

Generally, the formal method comprises two approaches, namely, property based and model-based. The property-based specification describes the operations performed on the system. In addition, it describes the relationship that exists among these operations. A property-based specification consists of two parts: signatures, which determine the syntax of operations and an equation, which defines the semantics of the operations through a set of equations known as axioms. The model-based specification utilizes the tools of set theory, function theory, and logic to develop an abstract model of the system. In addition, it specifies the operations performed on the abstract model. The model thus developed is of a high level and idealized. A model-based specification comprises a definition of the set of states of the system and definitions of the legal operations performed on the system to indicate how these legal operations change the current state.

Various advantages and disadvantages associated with a formal method model are listed in Table.

         Table Advantages and Disadvantages of Formal Methods Model



  1. Discovers ambiguity, incompleteness, and inconsistency in the software.
  2. Offers defect-free software.
  3. Incrementally grows in effective solution after each iteration.
  4. This model does not involve high complexity rate.
  5. Formal specification language semantics verify self-consistency.
  1. Time consuming and expensive.
  2. Difficult to use this model as a communication mechanism for non technical personnel.
  3. Extensive training is required since only few developers have the essential knowledge to implement this model.