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.>

An experience is presented with an automated test design tool for functional analysis and test derivation of distributed systems formally specified using Estelle, a description technique based on an extended finite-state machine model. The tool accepts a formal specification of the system and generates control, data flow graphs, and unparameterised test sequences. The tool has been used, on an experimental basis, for conformance test design of ISO File, Transfer, access and Management protocols.>