VERIFICATION
The previous two techniques are good for revealing errors in the simulated or actual system but usually cannot guarantee that the system satisfy a set of requirements. To apply formal verification techniques to a real-time system, we must first specify the system requirements and then the system to be implemented using an unambiguous specification language. Since the applications expert (programmer or system designer) is usually not knowledgeable in formal methods, a formal methods expert collaborates with the applications expert to write the requirements and system specification. Both experts work closely to ensure that the specifications reflect the real requirements and system’s behavior.
Once these specifications are written, the formal methods expert can verify whether the system specification satisfy the specified requirements using his/her favorite formal verification methods and tools. These formal methods and tools can show the satisfaction of all requirements or the failure to satisfy certain requirements. They may also pinpoint areas for further improvement in terms of efficiency. These results are communicated to the applications expert who can then revise the system specification or even the system requirements. The formal specifications are next revised to reflect these changes and can be analyzed again by the formal methods expert. These steps are repeated until both experts are happy with the fact that the specified system satisfies the specified requirements.
