Introduction

RELIEF, whose current version is RELIEFv3.5, has been developed under the supervision of Professor Hasan Ural of the Telecommunications Software Engineering Reseach Group (TSERG), Department of Computer Science, University of Ottawa.

Based on the Communicating Finite State Machine (CFSM) model of a protocol, the RELIEF validation methods explore the reachable global state space of the protocol to identify the logical errors such as blocking states, deadlocks, unspecified receptions, buffer overflows, and non-executable transitions. Besides the Conventional Reachability Analysis (CRA) method, the package also includes the implementations of a number of other methods, which are proved to yield a large reduction in the number of global states to be explored.

The protocol analyzers in RELIEF can be accessed through a text-based and menu-driven user interface. They can be also accessed by the Empirical Study (ES) [1] tool that takes a list of several hundred protocols synthesized by the Automatic Protocol Synthersizer (APS) [1] to generate the comparison of the performance of different methods. All of the tools are programmed in UNIX C and organized to form the system architecture of the package.

Written in Ottawa, October 1996

Edited: May 1997
Designer: Tuong M. Nguyen