| Abstract: | Communication protocols used in the field have always suffered from failures. Some of these faults are the result of design errors; others are the result of implementation errors. These errors dramatically increase maintenance cost and decrease software reliability. The best time to maintain software is during its design stage. A formal approach to developing a protocol is deemed necessary to improve the quality of communication software and to reduce maintenance costs. Protocol verification plays a major role in achieving these objectives; a protocol is first specified formally and then this formal specification is analysed using a computer-aided tool. PROTEAN is a software tool that verifies a protocol specified formally in Numerical Petri Nets. This paper describes the experience and practice of using PROTEAN to verify a complex protocol and then presents an evaluation of PROTEAN and its associated techniques in the light of protocol software development. The ISO FTAM protocol is used as a case study. |
