AG 1, AG 2   Info

AG Audience

-- Not specified --

-- Not specified --

Saarbrücken

Logical errors in finite state reactive systems are an important problem

for designers. They can delay getting a new product on the market or
cause the failure of some critical device that is already in use. My
research group has developed a verification method called temporal logic
model checking for this class of systems. In this approach
specifications are expressed in a propositional temporal logic, and
reactive systems are modeled as state-transition graphs. An efficient
search procedure is used to determine automatically if the
specifications are satisfied by the state-transition graph. The
technique has been used in the past to find subtle errors in a number of
non-trivial circuit and protocol designs.

During the last few years, the size of the reactive systems that can be
verified by model checking techniques has increased dramatically. By
representing sets of states and transition relations implicitly using
Binary Decision Diagrams (BDDs), we are now able to check examples that
are many orders of magnitude larger than was previously the case. In
this lecture we describe how the BDD-based model checking techniques
work and illustrate their power by verifying the Space Shuttle
Contingency Guidance Protocol. This protocol specifies what happens when
the shuttle has to abort its flight during take-off.


Interessenten/innen sind zum Vortrag herzlich eingeladen.

--email hidden

passcode not visible

logged in users only

Vortragsankuendigung
====================

Sprecher: Edmund M.Clarke
School of Computer Science
Carnegie Mellon University

Zeit: Montag, 04.05.1998, 10 h c.t.
Ort: DFKI SB, Geb. 43.1, Vortragsraum TURING (1.01)

Thema: Temporal Logic Model Checking


Abstract:
Logical errors in finite state reactive systems are an important problem
for designers. They can delay getting a new product on the market or
cause the failure of some critical device that is already in use. My
research group has developed a verification method called temporal logic
model checking for this class of systems. In this approach
specifications are expressed in a propositional temporal logic, and
reactive systems are modeled as state-transition graphs. An efficient
search procedure is used to determine automatically if the
specifications are satisfied by the state-transition graph. The
technique has been used in the past to find subtle errors in a number of
non-trivial circuit and protocol designs.

During the last few years, the size of the reactive systems that can be
verified by model checking techniques has increased dramatically. By
representing sets of states and transition relations implicitly using
Binary Decision Diagrams (BDDs), we are now able to check examples that
are many orders of magnitude larger than was previously the case. In
this lecture we describe how the BDD-based model checking techniques
work and illustrate their power by verifying the Space Shuttle
Contingency Guidance Protocol. This protocol specifies what happens when
the shuttle has to abort its flight during take-off.


Interessenten/innen sind zum Vortrag herzlich eingeladen.