Estelle: Formal Protocol Specification and Testing

Estelle Overview
Related Publications

» Back to Main Page «

Estelle Overview

To attain fully interoperable computer networks, one challenge that must be met is producing unambiguous formal specifications of any communication protocols that network employs. In the mid 1980's, Estelle was proposed as a formal description technique for the specification of communication protocols. Dr. Paul Amer has been actively involved in Estelle's development since 1985 when he spent a sabbatical year in Paris, France helping define Estelle's formal semantics and syntax with Piotr Dembinski and Stanislav Budkowski.

In 1989 with Professor Richard Tenney (Univ. of Mass, Boston) as Editor, Estelle was approved as an ISO International Standard. Based on communicating extended finite state machines, Estelle has a formal, mathematical, implementation-independent semantics. It is an expressive, well-defined, well-structured language that is capable of specifying distributed, concurrent information processing systems in a complete, consistent, concise and unambiguous manner.

There is little need to explore yet additional languages for formal specification; an international ISO standard based on ten years of study exists. The real challenge is to fully exploit the benefits of Estelle thereby making it as appealing and user friendly as possible to protocol specifiers. We need high quality software design tools based on Estelle: language-based graphical editors that facilitate the writing and modification of Estelle specifications, compilers that convert any Estelle specification to implementation code, simulators that emulate the message passing and extended finite state machine transition firing of any Estelle specification, etc. During the past five years, several Estelle tools that greatly facilitate the design, debugging, and testing of protocol specifications have been produced primarily at universities including Delaware. The best commercial Estelle tools available are the Estelle Development Toolset.

This project involves further developing new and existing Estelle tools and progressing these tools from research lab prototypes into successful, highly user-friendly software tools. Since 1994, the University of Delaware's Protocol Engineering Lab has assisted in the US Army's development of MIL-STD 188-220, the military standard for mobile combat network radios integrated with Internet protocols. We formally specified the Datalink and Network layers of 188-220 in Estelle, which resulted in more than fifty changes/improvements to the standard. Since 1996, with collaboration of the City College New York (CCNY), we have researched the problem of generating test cases automatically from these Estelle specifications in a restricted test environment, where a tester does not have complete control over and observability of the System Under Test (SUT). Within this effort, several theoretical problems have been encountered and solved, resulting in a number of journal and conference publications. By implementing the proposed methodology in software, we were able to generate and deliver test scripts to the Communications-Electronics Command (CECOM), which leads the US Army's activities to develop a 188-220B conformance test facility. The test sequences, which are currently being installed at a test facility in New Jersey, are realizable without timer interruptions and infeasible paths while providing a 200% increase in test coverage.

(Supported by Army Research Office (ARO), US Army CECOM, ARL Fed Research Lab in Telecommunications/Info Dist'n)

Related Publications

Authors	Title	Published	Paper
U. Uyar M. Fecko A. Duale P. Amer A. Sethi	A formal approach to development of network protocols: Theory and application to a wireless standard	CPWCSE 2001 - Concordia Prestigious Workshop on Communication Software Engineering, Concordia, 9/01	PDF
U. Puppala G. Meng P. Amer	A practical effort to generate conformance tests for MIL-STD 188-220B	SCI 2000, Orlando, 7/01	PS
P. Amer M. Fecko A. Sethi U. Uyar A. Duale	Formal specification and conformance testing of army communications protocols	Capstone Paper, Proc 5th ARL/ATIRP Conf., College Park, 3/01	PDF| PS
M. Fecko U. Uyar A. Duale  P. Amer	Efficient test generation for Army network protocols with conflicting timers	MILCOM 2000, Los Angeles, 10/00
M. Fecko U. Uyar A. Duale P. Amer	Test generation in the presence of conflicting timers	IFIP TestCom 2000, Ottawa, 8/00	PDF| PS
M. Fecko M. Uyar P. Amer A. Sethi T. Dzik R. Menell M. McMahon	A Success Story of Formal Description Techniques: Estelle Specification and Test Generation for MIL-STD 188-220	R. Lai, ed, FDTs in Practice, vol. 23 of Computer Communications, in press, Summer 2000	PDF| PS
M. Fecko M. Uyar A. Duale P. Amer	Efficient Test Generation for Army Network Protocols with Conflicting Timers	Proc 4th ARL/ATIRP Conf., College Park, 3/2000 (extended version published in IFIP TestCom'2000, Ottawa, Canada)	PDF| PS
M. Fecko M. Uyar A. Amer A. Sethi	Conformance Testing in Systems with Semicontrollable Interfaces	S. Budkowski and E. Najm, eds, Protocol Engineering: Part 2, vol. 55(1-2) of Annals of Telecommunications, 1-2/2000	PDF| PS
M. Fecko M. Uyar P. Amer A. Sethi	Using Semicontrollable Interfaces in Testing Army Communications Protocols: Application to MIL-STD 188-220B	MILCOM'99, Atlantic City, NJ 11/99	PDF| PS
M. Uyar M. Fecko A. Sethi P. Amer	Testing Protocols Modeled as FSMs with Timing Parameters	Computer Networks, 31(18):1967-1998, 9/1999	PDF| PS
M. Fecko M. Uyar A. Sethi P. Amer	Issues in conformance testing: multiple semicontrollable interfaces	FORTE/PSTV '98, Paris 11/98	PDF| PS
M. Fecko U. Uyar P. Amer A. Sethi	Optimum test sequence generation from Estelle specifications	Estelle '98, Paris, 11/98	PDF| PS
P. Amer A. Sethi M. Fecko M. Uyar T. Dzik R. Menell M. McMahon	Using Estelle to evolve MIL-STD 188-220	Estelle '98, Paris, 11/98	PDF| PS
U. Uyar M. Fecko A. Sethi P. Amer	Generation of realizable conformance tests under timing constraints	Proc MILCOM '98, Boston, 10/98	PDF|PS
M. Uyar M. Fecko A. Sethi P. Amer	Minimum-cost solutions for testing protocols with timers	Proc IEEE Int'l Performance, Computing, and Comm Conf. (IPCCC), Phoenix, 2/98	PDF|PS
M. Fecko P. Amer A. Sethi M. Uyar T. Dzik R. Menell M. McMahon	Formal design and testing of MIL-STD 188-220A based on Estelle	Proc MILCOM '97, Monterey, CA, 11/97	PDF|PS
P. Amer A. Sethi M. Fecko M. Uyar	Formal design and testing of army communication protocols based on Estelle	Proc 1st ARL/ATIRP Conf., College Park, 1/97, 107-114	PDF|PS
P. Amer G. Burch A. Sethi D. Zhu T. Dzik R. Menell M. McMahon	Estelle specification of MIL-STD 188-220A data link layer	Proc MILCOM '96, McLean, VA, 10/96	PDF|PS
H. Li P. Amer S. Chamberlain	Estelle specification of MIL-STD 188-220: Interoperability standard for digital message transfer device subsystems	Proc MILCOM '95, San Diego, 11/95.	PDF|PS
G. Burch P. Amer S. Chamberlain	Performance evaluation of MIL-STD 188-220: Interoperability standard for digital message transfer device subsystems	Proc MILCOM '95, San Diego, 11/95.	PDF|PS
P. Kalyanasundaram P. Amer	Protocol test case visualization	6th IFIP Workshop on Protocol Test Systems (IWPTS), Pau, France, 9/93, 201-218
P. Amer D. New	Protocol visualization in Estelle	Computer Networks and ISDN Systems, 25(7), 2/93, 741-760.
S. Chamberlain P. Amer	Formal specification of real-time constraints in Estelle	Reseaux et Informatique Repartie, 2(2), 1992, 113-134
P. Amer W. Chun	Improvements on UIO sequence generation and partial UIO sequences	Protocol Specification, Testing, and Verification, XII, (Orlando), J. Linn, M. Uyar (eds), North-Holland, Amsterdam, 1992, 245-260	PDF
S. Chamberlain P. Amer	Estelle enhancements to support the specification of distributed systems	Proc Computer Networks '91, Wroclaw, Poland, 6/91
S. Chamberlain P. Amer	Broadcast channels in Estelle	IEEE Trans on Computers, C-40(4), 4/91, 423-436.
D. New P. Amer	Adding graphics and animation to Estelle	Information and Software Technology, 32(2), 3/90, 149-161
P. Amer F. Ceceli	Estelle formal specification of ISO virtual terminal	Computer Standards and Interfaces, 9(2), 12/89, 87-104