ARTES
-------------------------------------------------

 

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.

  ---------------------line----------------------------
  Strategic Research