EPVD - AN INTERACTIVE PROTOCOL SPECIFICATION AND VALIDATION ENVIRONMENT IN ESTELLE FORMAL SPECIFICATION

The Extended Protocol Validation Development System (EPVD) is extended on PVD [1]. The PVD provides an interactive protocol specification and validation software environment on finite state machine (FSM) model. EPVD extends an Estelle environment into PVD, then provides the specification and validation of communication protocol in Estelle formal specification. It provides a graphic-interface for user to specify the modules and transitions of communication protocol. By ultilizing our developed intra-module combination/validation technique, we can easily combine and validate these transitions. A FSM and the logical correctness of associated these transitions can also be found as well. The inter-module combination/validation algorithm is developed to combine and to validate the FSMs of module, and in turn, is used to find a FSM and the logical properties of their communications. EPVD implements those approaches with several tools. Users could use these tools to specify a communication protocol with either FSM model or Estelle model, and to validate the intra-entity and inter-entity communications. This system has been used to design and to validate an ABP specification [4], and the result is to be reported.