|
Abstract : |
This dissertation investigates the use of formal verification to demonstrate the correctness of hard real-time systems, that is, computer systems in which programs are required to respond to events from their environments within realtime deadlines. A mathematical formalism, higher order logic, is used to prove that programs react in a correct and timely manner to identified real-time events of their environments. Higher order logic is used both to describe the behaviour of programs written in a simple, imperative program language with asynchronous communication primitives and to specify the environments with which programs interact. It is assumed that the implementation of the program language allows the exact time taken to execute commands to be calculated. It is then proved that a specification of programs and environments satisfies requirements which are also stated in higher order logic. The HOL system, a theorem prover for higher order logic, has been used to type check specifications and mechanize verification proofs., |
