Formal Methods For Mobility Standards

Daniel Amyot, Rossana Andrade, Luigi Logrippo, Jacques Sincennes, Zhimey Yi
University of Ottawa

Abstract

Precise specification and exacting verification and validation of
protocol standards are essential for their successful development and
implementation. Currently, several languages (called FDTs for Formal
Description Techniques) are available to address this issue. FDTs
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 FDTs considered are, in alphabetical
order: the Abstract Syntax Notation 1 (ASN.1), the Language of Temporal
Ordering Specifications (LOTOS), Message Sequence Charts (MSCs), 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 (UCMs).

Keywords: Mobility Standards, Formal Methods, Validation and Verification,
		Wireless Intelligent Network