The Verus Language: Representing Time Efficiently with BDDs
S. Campos and E. Clarke
There have been significant advances on formal methods to verify
real-time systems recently. Nevertheless, these methods have not yet
been accepted as a realistic alternative to the verification of
industrial systems. One reason for this is that formal methods are
still difficult to apply efficiently. Another reason is that current
verification algorithms are still not efficient enough to handle many
complex systems. This work addresses this problem by presenting a
language designed especially to simplify writing real-time
programs. It is an imperative language with a syntax similar to
C. Special constructs are provided to allow the straightforward
expression of timing properties. The familiar syntax makes it easier
for non-experts to use the tool. The special constructs make it
possible to model the timing characteristics of the system naturally
and accurately. A symbolic representation using BDDs, model checking
and quantitative algorithms are used to check system timing
properties. The efficiency of the representation allows complex
realistic systems to be verified by the method as evidenced by the
examples verified such as the aircraft controller discussed in the
paper.
Symbolic Techniques for Formally Verifying Industrial Systems
Verifying the Performance of the PCI Local Bus
using Symbolic Techniques
Verus: A Tool for Quantitative Analysis of Finite-State
Real-Time Systems
Symbolic model checking is a technique for verifying finite-state
concurrent systems that has been extended to handle real-time systems.
Models with up to 10E30 states can often be verified in minutes.
In this paper, we present a new tool to analyze real-time systems,
based on this technique. We have designed a language, called
Verus, for the description of real-time systems. Such a description
is compiled into a state-transition graph and represented symbolically
using binary decision diagrams. We have developed new algorithms for
exploring the state space and computing quantitative information
about the system. In addition to determining the exact bounds on the
delay between two specified events, we compute the number of
occurrences of an event in all such intervals. This technique allows
us to determine performance measures such as schedulability, response
time, and system load. Our algorithms produce more detailed
information than traditional methods. This information leads to a
better understanding of the behavior of the system, in addition to
verifying if its timing requirements are satisfied. We integrate
these ideas into the Verus tool, currently under development. To
demonstrate how our technique works, we have verified a robotics
control system. The results obtained demonstrate that our method can
be successfully applied in the analysis of real-time system designs.
Computing Quantitative Characteristics of Finite-State
Real-Time Systems
Current methods for verifying real-time systems are
essentially decision procedures that establish whether the system
model satisfies a given specification. We present a general method for
computing quantitative information about finite-state real-time
systems. We have developed algorithms that compute exact bounds on the
delay between two specified events and on the number of occurrences of
an event in a given interval. This technique allows us to determine
performance measures such as schedulability, response time, and system
load. Our algorithms produce more detailed information than
traditional methods. This information leads to a better understanding
of system behavior, in addition to determining its correctness. We
also show that our technique can be extended to a more general
representation of real-time systems, namely, timed transition graphs.
The algorithms presented in this paper have been incorporated into the
SMV model checker and used to verify a model of an aircraft control
system. The results obtained demonstrate that our method can be
successfully applied in the verification of real-time system designs.
S. Campos, E. Clarke and M. Minea
The design of correct computer systems is extremely difficult.
However, it is also a very important task. Such systems are frequently
used in applications where failures can have catastrophic
consequences, or cause significant financial losses. Simulation and
testing are the most widely used verification techniques, but they can
only show the presence of errors and cannot demonstrate correctness.
Until lately formal methods were too expensive to be used in
industrial problems, but recent research has made it possible to apply
formal techniques to the verification of complex real-world systems.
Symbolic model checking is an example of such a technique that
has been successful in verifying large finite-state systems. It has
also been extended to produce timing and performance information.
These properties are extremely important in the design of
high-performance systems and time-critical applications. A more
detailed analysis of a model is possible using these extensions than
by simply determining whether a property is satisfied or not. We
present algorithms that determine the exact bounds on the delay
between two specified events and the number of occurrences of another
event in all such intervals. To demonstrate how our method works, we
present two complex examples: the verification of the Futurebus+ cache
coherence protocol and the timing analysis of the PCI local bus.
These results show the usefulness of symbolic model checking in
analyzing modern industrial designs.
S. Campos, E. Clarke, W. Marrero and M. Minea
Symbolic model checking is a successful technique for checking
properties of large finite-state systems. This method has been used to
verify a number of real-world hardware designs. This methodology,
however, is not able to determine timing or performance properties
directly. Since these properties are extremely important in the design
of high-performance systems and in time-critical applications, we have
extended model checking techniques to produce timing information.
These results allow a more detailed analysis of a model than is
possible with tools that simply determine whether a property is
satisfied of not. We present algorithms that determine the exact
bounds on the delay between two specified events and the number of
occurrences of another event in all such intervals. To demonstrate how
our method works, we have modelled the PCI local bus and analyzed its
temporal behavior. These results show the usefulness of this technique
in analyzing complex modern designs.
S. Campos, E. Clarke, W. Marrero and M. Minea
S. Campos, E. Clarke, W. Marrero, M. Minea and H. Hiraishi
Back to the main page