This paper introduces some formal methods for specification and verification. This papers also assesses the state of the art in specification and verification and highlights advances in model checking and theorem proving and also describes some successful case studies and well-known tools. This paper outlines the definition of specification and outlines two methods for Verification, namely Model Checking and Theorem Proving with some accompanied examples.

Specification is the process of describing a system and its desired properties. It serves as a companion document to the system’s source code but at a higher level of description. Some notable examples of this are IBM’s customer Information Control System and Avionic Software of Lockheed, and TCAS. One noticeable point in the examples briefed in this section of the paper is that most of the applications seem to be very mission critical. These are the ones in which every small mistake could prove to be very expensive. But in a lot of other non-mission critical applications, a specification document is simply an act of writing things down precisely. I do not believe that the specifications can be written precisely to reflect requirements either because of changes in requirements and because of lack of creativity. In this case specifications have to refined may times before the design or actual implementation can begin. In the absence of refinement, incorrect specs could worsen the same problems specifications were set to solve.

The process of Verification has two well-established approaches, 1)Model Checking 2)Theorem Proving. Model Checking is a technique of checking for a desired property that should hold in a model using an exhaustive state space search. The two general approaches to model checking that are in practice according to this paper are 1)temporal model checking in which an efficient search procedure is used to check if a given finite state transition system is a model for the specification. 2)an approach in which the system and the specification are modeled as an automaton and compared.

It seems like the formal methods of specification and the exhaustive methods of verification are more suitable to very mission critical applications in air-force, space etc related areas. Barring some commercial areas like commercial avionics and medical applications etc, most of the commercial products are not so mission-critical and probably don’t justify the costs of generating a formal specification and refining it and verifying it so exhaustively. Besides there are not many tools available that make these processes less expensive and less time-consuming. May be when tools like that are available, then it really makes sense to strictly follow the formal methods.

While specifications can help analyze the product and describe its desired properties precisely, things like User Interfaces are still very difficult to specify and I think this is one area where formal methods of specification fail.

This paper defines the terms Specifications and Requirement and illustrates how requirements can be derived from specification with an example. A requirement states desired relationship in the environment – relationships that will be brought about or maintained by the machine. A specification describes the behavior of the machine at its interface with the environment.

The process of deriving specifications from requirements involves: Refining requirements by removing all the phenomena that is inaccessible to the machine, designating environment phenomena in requirement and specification descriptions and deciding on the designations that are specific to the environment, by identifying the phenomena shared between the machine and the environment, determining where the control of the phenomena resides, Indicating environment descriptions using a Finite-State automaton.

This is a very neat and simple scheme of converting the requirements into specifications. However, I am skeptical about the scaling capability of this procedure. The paper illustrates with a very simple example where there are only tow agents the machine and environment. I doubt that most of the real world commercial applications are as simple as the one illustrated in the paper. It would be interesting to see how this procedure applies to applications that are heavily user driven or to any applications of Artificial Intelligence where the number of states could be really huge. Nevertheless, this is a simple procedure that can be easily learned and applied to simple applications.

This paper describes an approach to writing requirements specifications for process-control systems, a specification language that supports this approach, and an example application of the approach and the language on an industrial Aircraft Collision Avoidance System. This paper outlines an approach to generating requirements specification by building one state-based model that includes all of the information needed to describe the blackbox behavior of the components of the system and the interface between the components.

A typical process-control system can be divided into four types of components: the process, sensors, actuators, controller. The blackbox behavior of the controller is specified using a State machine model. The state machine model of the controller is iteratively fine tuned during requirements specification development to be coherent with the current understanding of the real world process and the required controller behavior.

This paper gives the opinions of different people from academia as well as industry. Some of them identify the reasons for industry’s reluctance to adopt formal methods. Some others suggest solutions to these problems.

The problems are 1)Myths that formal methods can guarantee correct hardware and software, eliminating the need for testing or misconceptions that formal methods are difficult to use, that they delay the development process and raise development costs. 2) Lack of recommendations from Standards bodies to use formal methods in certain classes of applications. 3)Lack of tool support and tool integration. 4) Lack of adequate examples to follow and learn from 5) Lack of education and training. 6)A chasm that exists between academia and industry. The two group’s perception of formal methods as two different concepts.

Some solutions are: 1)An ongoing forum in which academics and practitioners meet to discuss their views of software. 2)Using formal methods in a lighter way. 3)Providing powerful tools 4)Using formal verification to find bugs. 5)By targeting formal methods towards solving problems not handled by other means. 6)Making researchers apply their work to real problems.

I have always thought that following formal methods is time-consuming and expensive. I have heard a lot of people in the industry say that the academia is always lagging behind the industry. While we all know that this is a misconception, unless are a lot of powerful and easy-to-use tools available in the commercial world, this misconception is going to remain.