Title: Event Order Abstraction for Parametric Real-Time System Verification

Speaker:  Shinya Umeno

Place: 	32-G531
Time: 	1-2:30pm
Date: 	Friday, February 15, 2008
 
Abstract:
We present a new abstraction technique, event order abstraction (EOA),
for parametric safety verification of real-time systems in which ``correct
orderings of events'' needed for system correctness are preserved by
timing dependent behavior of the systems.
  By using EOA, one can separate the task of verifying a system into two
parts: 1. A derivation of timing parameter constrains for correct orderings
of events in the system; and 2. A safety property verification of the system
given that those correct orderings are preserved.
  We first identify bad event orderings, and then automatically derive a set
of timing constraints under which the system does not exhibits the
identified bad event orderings. We then examine whether a discretized
system model in which all timing behaviors are abstracted away satisfies
a desirable safety property under the assumption that the identified bad
event orders do not occur in the system execution. This examination is
done by a model-checking. We successively refine this assumption by
extracting additional bad event orders from a counterexample obtained
from the model-checking, until we successfully model-check the
discretized model.
   We summarize three case studies, a train-gate system, a biphase mark
protocol, and the Fischer mutual exclusion algorithm.