The Inverse Method: Parametric Verification of Real-time Embedded Systems

Introduction

The importance of computer systems has dramatically increased in recent decades. Critical systems, involving human lives, need to be perfectly reliable, with a total absence of any inappropriate behavior, such as failures or unexpected sequences of actions.

Let us consider the case of hardware verification. When we analyze synchronous clocked digital circuits, it is possible to separate the functional analysis from the timing analysis: the clock cycle is determined by computing the accumulated delays along the longest path from input to latches, and, assuming that the cycle time is large enough, the functional verification can proceed by ignoring gate and wire delays and by treating the whole circuit at the abstraction level of an untimed finite state automaton. Symbolic methods of model checking relying on efficient and compact representation and manipulation of sets of states are thus very useful for verifying the correctness of hardware circuits.

Such a separation between logic and time is rarely possible when we want to analyze computerized systems that are often made up of dozens of reactive components that are in permanent interaction all together and with the physical environment, with few or no mechanisms of global synchronization. In this context, the delays taken by the individual tasks and their logical interdependency have an immediate impact on the global order in which the actions are taken, and on the functionality of the system. Many counterintuitive ...