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 modelbased. The propertybased specification describes the operations performed on the system. In addition, it describes the relationship that exists among these operations. A propertybased 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 modelbased 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 modelbased 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
Advantages 
Disadvantages 


Dinesh Thakur holds an B.SC (Computer Science), MCSE, MCDBA, CCNA, CCNP, A+, SCJP certifications. Dinesh authors the hugely popular Computer Notes blog. Where he writes howto guides around Computer fundamental , computer software, Computer programming, and web apps. For any type of query or something that you think is missing, please feel free to Contact us.
Basic Courses
Advance Courses