Formal methods for mobility standards

Precise specification and exacting verification and validation of protocol standards are essential for their successful development and implementation. Currently, several languages (called FDT for formal description techniques) are available to address this issue. FDT have reached various degrees of acceptance, but their use in standard development in North America has been limited. This paper represents an attempt towards divulging the knowledge of what exists and how it can be used effectively based on the methods that were found most useful in our work on mobility protocols. The FDT considered are, in alphabetical order: the Abstract Syntax Notation 1 (ASN 1), the Language of Temporal Ordering Specifications (LOTOS), Message Sequence Charts (MSC), the Specification and Description Language (SDL) and the Tree and Tabular Combined Notation (TTCN). Also considered is a new, emerging non-formal technique, called Use Case Maps (UCM)