@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading(A Quantitative Approach to the Formal Verification
of Real-Time Systems)
@heading(CMU-CS-96-199)
@center(@b(Sergio Vale Aguiar Campos))
@center(September 1996 - Ph.D. Thesis)
@center(FTP: Unavailable)
@blankspace(1)
@begin(text)

The task of checking if a computer system satisfies its timing
specifications is extremely important. These systems are often used in
critical applications where failure to meet a deadline can have
serious or even fatal consequences. This work proposes an efficient
method for performing this verification task. The method is based on
temporal logic model checking, a technique for verifying concurrent
reactive systems. In the proposed technique, a real-time system is
modeled by a state-transition graph represented by binary decision
diagrams. Efficient symbolic algorithms exhaustively explore the state
space to determine whether the system satisfies a given specification.

In addition to accepting an explicit timing constraint, and checking
if it is satisfied, our approach computes quantitative timing
information such as minimum and maximum time delays between given
events. These results provide insight into the behavior of the system
as well as assist in the determination of its temporal correctness.
The technique evaluates how well the system works or how
seriously it fails, as opposed to only if it works or not, allowing a
much richer analysis than previous methods. Response time to events,
schedulability of a task set and system performance are examples of
information produced by our algorithms. They also provide insight into
how changes in the parameters affect global behavior and allow
fine-tuning of the system based on these results.

These techniques have been used in the verification of several
industrial real-time systems such as an aircraft controller, a
robotics system and the PCI local bus, demonstrating that the method
proposed is efficient enough to be used in real-world designs. The
examples show how the information produced can assist in designing
more efficient and reliable real-time systems.

@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Real-time systems, formal verification, symbolic model
checking, binary decision diagrams, rate-monotonic scheduling, schedulability,
quantitative timing analysis, Verus language, CTL, LTL, FDDI, Futurebus, 
PCI Local Bus, robotics controller, aircraft controller>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(240 pages)])