As more complex computational systems are used within critical applications, it is becoming essential that these systems are formally specified. Such specifications are used to give a precise and unambiguous description of the required system. While this is clearly important in criticial systems such as industrial process management and air/spacecraft control, it is also becoming essential when applications involving E-commerce and mobile code are developed. In addition, as computational systems become more complex in general, formal specification can allow us to define the key characteristics of systems in a clear way and so help the development process. Formal specifications provide the basis for verification of properties of systems. While there are a number of ways in which this can be achieved, the model-checking approach is a practical and popular way to verify the temporal properties of finite-state systems. Indeed, such temporal verification is widely used w
ithin the design of critical parts of integrated circuits, has recently been used to verify parts of the control mechanism for one of NASA’s space probes, and is now beginning to be used to verify general Java programs.
|