Analysis and testing of application layer protocols with an application to FTAM

An experience with formal specification, analysis, and testing of an application layer protocol is presented. The ISO file, transfer, access, and management (FTAM) protocol is chosen due to its potential for widespread use. The specification language used was the ISO standard Estelle. This tool generates control and dataflow graphs of the specification and derives unparameterized test sequences for each function identified by the user. The authors describe formal specification of application layer protocols in Estelle and translation of ASN.1 data definitions into Estelle data types. The test design tool is used to obtain functional decomposition of the control and dataflow graphs. This way unparameterized test sequences are obtained. These sequences lead to a complete test suite obtained by parameterization which must be the next step. Analysis of the control and dataflow graphs leads to the derivation of several properties that most of the application layer protocols must possess. The identified properties are shown to simplify the test design process