VII.1 Introduction
Introduction [Slide 307]
Assuring the correctness of hardware and software systems, like digital circuits and
communications protocols, is a difficult task.
- Complexity of the system.
- Size of the system.
- Requirements that need to be satisfied.
Several techniques have been proposed to assure the correctness of systems:
- testing (simulators, debuggers, etc.),
- formal methods, (theorem provers, proof checkers and model checkers),
- runtime verification (simulators + theorem checkers).
- System: collection of communicating agents (processes)
- State: variables and communication links
- Behaviour: sequence of states (interval)
- Property: set of behaviours