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).
- This paper represents an attempt towards divulging knowledge of what exists and how it can be used effectively to describe, specify, and validate standards for mobile telephony. The techniques evaluated are UCMs, MSCs, LOTOS, ASN.1, SDL, and TTCN.
- Please feel free to discuss this article directly on this page. Constructive comments are welcomed! Please sign your TWiki name.
| Title || Formal Methods for Mobility Standards |
| Authors || D. Amyot, R. Andrade, L. Logrippo, J. Sincennes, and Z. Yi |
| Type || Conference |
| Conference/Journal Title || IEEE 1999 Emerging Technology Symposium on Wireless Communications & Systems, Dallas (TX), USA |
| Volume/Number || |
| Editors || |
| Publisher || |
| Month || April |
| Year || 1999 |
| Pages || 14.1 - 14.7 |
| DOI || 10.1109/ETWCS.1999.897332 |
| Keywords || UCMs, MSCs, LOTOS, ASN.1, SDL, TTCN |