SENG 611: Requirements Engineering Summary of Lecture on Formal Specifications	Omolade Saliu

Formal Specifications:

Formal specifications are used to describe a system in a language whose vocabulary, syntax and semantics are formally defined using mathematical notations. Formal specifications can be used to build model of a system in mathematical way, and proof that the system would work as desired, even before design. They can be analyzed mathematically and the consistency and completeness of the specification can be demonstrated. Formal specification are particularly suitable for systems with stringent safety, reliability or security requirements.

Two approaches have been used to write formal specifications for non-trivial systems (Ian Somerville, 2001):
     - Algebraic approach: systems are described in terms of operations and their relationships e.g., Larch and Lotos.
     - Model-based approach: model of system built using mathematical constructs like sets and sequences e.g., Z, VDM, CSP

Formal specifications are precise, clarity and unambiguous in describing a system. However, the most potent argument for developing a formal specification is error-detection (Anthony Hall, 1990).

Critical Comments:

Formal specifications have been used to achieve desired quality objectives in safety-critical systems like air traffic control, space exploration, nuclear power plant, and so on. Outside these specialized domains (and other similar critical systems) identified, it is highly unlikely that formal specification will gain wide acceptance in developing majority of systems, because they require specialized expertise and may not offer significant cost or quality advantage over other approaches in the long run. I would say that, many other software engineering techniques and processes have resulted in improvements that match quality requirements of many commercial and industrial systems, and investment in formal methods may be difficult to justify.

Another burning factor is the changing market demand, which has driven software project managers to consider time-to-market a very great concern. There is absolutely no point having a well-proven and quality-assured product released when the market no longer needs it. Customers may sometimes compromise quality factor to a level, so long rapid delivery is achieved. Also, techniques for rapid delivery would not benefit much from using formal specifications.

During the lecture, it was stated that cost of carrying out full formal specification can be very high (Rob Kremer, 1998). This may not be the case in all situations. Formal methods can be cost-effective for a safety-critical systems, because it would avoid high validation costs and costs of system failures in the long run.

Formal specifications helps to eliminate ambiguity of natural language in requirements specification, but I doubt if there would ever come a time that users get to appreciate formal methods of specification, because of lack of familiarity and skill level required.

There are several recommendations on where formal specification should actually come in. One of such is for formal specification to stand somewhere
between software system requirements and software design specifications (Ian Sommerville, 2001). They do not have to include implementation detail but should present a complete mathematical model of the system or part of the system under consideration. This implies that formal methods would be most effective when the requirements are already established, which makes a lot of sense. After all, we cannot have mathematical models of what we cannot understand. A good suggestion is to use formal specification synergistically with other development techniques, only to model sub-system that requires high security, safety, etc.

References:

(Anthony Hall, 1990). Seven Myths of Formal Methods. IEEE Software, 7(5), pp. 11-20, Sept. 1990.
(Ian Sommerville, 2001).  Software Engineering, 6^th Edition, Addison-Wesley, 2001.
(Rob Kremer, 1998). Formal Specification. University of Calgary.  http://sern.cpsc.ucalgary.ca/courses/SENG/611/W04/FormalSpecs.html 

	SENG 611: Requirements Engineering
Omolade Saliu Last updated:21/02/04	Back to Omolade Saliu's Home Page