
Relative Timing Based Verification of
Concurrent Systems
The thesis presents a new theory and methodology for the formal
verification of safety properties in timed systems. The correct
operation of such systems not only depends on a set of functional
properties but also on certain assumptions about the delays of the
components of the system and the response times of the environment in
which the system operates. The verification of this type of systems
typically involves several computationally hard problems. In particular,
the combinatorial state explosion problem becomes exacerbated by the
time dimension.
The theory that supports the proposed verification approach extends the
conventional BDDbased symbolic methods to the verification of timed
systems, modeled by means of timed transition systems. The theory is
based on the relative timing paradigm, which instead of considering
exact time differences in the occurrence of events, considers the effect
of delays in terms of relative orderings between events. For example, in
order to guarantee that a race is not propagated in a digital circuit,
it is often sufficient to check that certain signal switches before
another, instead of identifying the exact instants of time in which both
signals switch. Moreover, the timing information does not need to
computed for the overall system, but only locally for the part of the
system involved in the proof or disproof of a given property. This is
possible thanks to a crucial observation, that the set of executions of
a transition system can be covered by a set of partial orders. As a
consequence, only a subset of the events of the system is involved in
the proof of a property and the timing analysis can be carried out very
efficiently.
Conventional methods for the verification of timed systems rely on the
computation of the exact timed state space of the system as the first
step of the analysis. Although efficient techniques have been devised to
overcome the complexity issue (e.g. difference bound matrices), symbolic
methods cannot be easily applied. Thus, the combinatorial timestate
explosion problem often limits the applicability of such methods to
moderatesize systems.
Instead, the approach proposed in the thesis relies on an incremental
refinement of the untimed state space of the system, so that timing
information is incorporated as soon as it is needed. The timing
information is derived by an efficient offline timing analysis over
small sets of events. The refined state space is captured under the
model of lazy transition system, which allows an efficient
representation of the timed domain using conventional symbolic methods.
As a consequence, the approach can be potentially applied to bigger
systems or to systems with more level of detail, than those that can be
handled by similar methods for the verification of timed systems.
Moreover, the incremental nature of the approach provides a good way to
obtain at least partial results even on systems for which complete
solutions could be too complex to compute.
A key feature of the proposed verification approach is that not only
proves or disproves the correctness of a timed system. If the system is
correct the set of relative timing relations used for the proof are
provided. Such relations constitute a set of sufficient timing
constraints that guarantee the correctness of the system. On the other
hand, if the system is incorrect, a counterexample failure trace is
provided. The most important aspect of all this feedback is that it can
be used as valuable backannotation information along the design process.
This feature, which allows to bridge the gap between verification and
design, constitutes another differential aspect of our verification
approach when compared to other equivalent verification methods.
The verification approach has been fully implemented in an experimental
CAV tool called TRANSYT. The tool can handle hierarchical and
distributed modular systems which can interoperate by a variety of
communication mechanisms. TRANSYT has successfully proved its
functionality as well as the validity of the overall verification
approach, by verifying a number of timed asynchronous circuits with up
to more than 10^{6} untimed states. The experiments cover, for
example, the verification of: complexgate decompositions in quasispeedindependent
asynchronous circuits, delayreset domino circuits, pulsebased systems,
circuits optimized for speed using timing assumptions, etc. Additionally,
compositional verification methods have been combined with the basic
verification approach in order to tackle the size/complexity issues
involved in the verification of complex timed systems. Thus,
abstractions, assumeguarantee reasoning and mathematical induction have
been used to prove the correctness the IPCMOS architecture. It is a
scalable pipelined architecture which is aimed to the interconnection of
different clock zones in a system.
Thanks to the rather theoretical nature of the proposed verification
approach, its potential applicability covers a wider range of systems
than those cited above, such as: custom transistorlevel circuits that
exploit the technology limits for performance, complex digital
structures where synchronization is a crucial issue (e.g. dynamic MOS),
asynchronous and GALStype systems, realtime systems, etc.

