• home
• current students
• graduate
• events

Presenter: Dr. Richard Trefler - AT&T Labs Research, Florham Park, NJ - Faculty Applicant
Supervisor: Dr. R. Nigel Horspool, Professor and Chair, Department of Computer Science

Date: Mon, April 22, 2002
Time: 13:30:00 - 14:30:00
Place: Engineering Office Wing Building (EOW), Room # 430

ABSTRACT

ABSTRACT:

Automated reasoning tools, such as model checkers, take a mathematically precise specification of a program and automatically verify that it does what it is supposed to. They offer system designers key benefits, such as engendering design precision at the earliest stages of development, and identifying bugs in systems that do not function as intended. In this talk, I will present recent work in compositional reasoning and abstraction, two important strategies used in model checking.

Many systems are too large to check directly, and compositional reasoning is an essential method for reasoning about large systems by breaking them into their component parts. Accurate decomposition of system properties has been a difficult problem, however. In recent work, we used Synchronous Regular Timing Diagrams (SRTDs), a visually intuitive specification language, to write program specifications used in model checking, with very positive results. Since SRTDs are inherently compositional, we found that they could be used very naturally and effectively even for large systems, and we formulated a sound and complete proof rule allowing such systems to be model checked compositionally.

Abstraction is another important technique that we have used to model check ECLIPSE, an IP telephony software system that generates a potentially infinite state system. Infinite state systems are impossible to model check as such, so we used abstraction in a novel way to produce a checkable, finite state system. In subsequent trials, the model checker successfully detected system errors, demonstrating the efficacy of the abstraction.

In short, recent refinements in both compositional reasoning and abstraction are helping to make model checking a more usable and effective tool in the designer's arsenal, as shown by the promising results realized in trials of industrial systems.