ARTES Summerschool
Presentations, SNART 99
23 - 27 August 1999
Validation of Dependable Real-Time Protocols - A Formal Method Approach
Neeraj Suri
Dept. of Computer Engineering, Chalmers University of Technology
Abstract
The traditional use of formal methods is for correctness checking or
verification. Given the limitations in state space coverage provided by conventional
validation techniques (and the prohibitive cost/time requirements for testing), we
discuss
the use of formal verification procedures to aid validation of composite
dependable
and real-time protocols through identification of very specific test cases
to check the protocols.
The talk will present an overview on validation techniques, on the use of
formal
methods at the protocol level, as well as the utility & limitations of
formal methods
for real-time protocol analysis. The development of a formal validation
approach/toolset
will then be discussed. The actual analysis of a fault tolerant RMA
protocol will be discussed as a case study to show the capabilities of such
a formal validation approach.
Biography
Neeraj Suri
obtained the PhD degree from the University of Massachusetts at
Amherst.
He is the Saab Professor of Dependable and Robust Real-Time Systems at the
Dept.
of Computer Engineering at Chalmers University, Sweden.
His research interests are in developing the theory, issues in formal
verification, validation
and experimentation in the composite areas of dependable, real-time
distributed systems.
His research in these areas are currently supported by US Dept. of Defense
(DARPA), NASA, NAWC, ONR, and by NSF through a CAREER research award.
He is on the editorial board for the IEEE Transactions on Parallel and
Distributed Systems,
a senior member of the IEEE Computer Society and a member of the IFIP 10.4 WG
on Dependable Computing.
|