O'Reilly logo

The Inverse Method: Parametric Verification of Real-time Embedded Systems by Romain Soulat, Etienne André

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required