Software has manifested itself as an essential component in a lot of the systems we use today. Taking the aeronautical domain as an example, we realize that due to the increasing number of commercial flights and the tremendous volumes of passengers they carry, there is an inspiration to increase safety measures within the airline field. In conjunction with all the other factors affecting air travel, the reliability of this air transportation service is dependent on the on-board computers as well as on the control tower navigation systems. Therefore, computers and the software that runs on them, dictate the reliability of the flights and the safety of the passengers using them. Any errors that the software might induce, can translate into disastrous consequences for the plane and the passengers it carries.

Till date, there have been a number of air accidents where software errors such as failure to display information, incorrect application of control mechanisms etc, have been listed among the causes of air accidents.

One method for preventing software errors from translating into disastrous endings is to prevent software errors from occurring in the first place. To that extent, one has to study the kind of software systems that exist in planes and find ways for eliminating errors. Formal verification techniques have proved to be a cost effective method for finding defects in hardware designs. The application of this formal technique has been less profound in the software domain. The problem is not the use of formal methods on formal models of software, but the generation of those models. We need to take the pieces of code generated by software developers and translate them into specification languages accepted by the current verification tools. Most verification tools accept specification languages designed for the simplicity of their semantics, whereas most development is done with general purpose programming languages which might lack that simplicity. This makes it hard to achieve a translation, and instead we get a transformation. The accuracy of the transformation is the essential quality that is sought after in designing these model builders.

A tool (VAT tool) to transform VHDL code into a corresponding formal model has been designed and implemented by the ESL group. The code once converted to a formal model by the tool, can have model checking applied to it and therefore can be tested against certain constraints, like timing and absence of deadlock, and verified to adhere to them. The tool has a clearly defined interface and uses an intermediate notation to allow the flexibility of using any one of the many model checker formal notations out there. A different translator is needed for each target verifier language, but the translator only transforms the already extracted formal model into the appropriate notation and hence is simple to construct. In conclusion, it is not clever model checkers that are missing, but clever model builders.