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