Telecommunication protocol standards have in the past and typically
still use both an English description of the protocol (sometimes also
followed with a behavioural SDL model) and an ASN.1\cite {6} specification of
the data-model, thus likely making the specification incomplete.
ASN.1 (Abstract Syntax Notation One) is an ITU/ISO data definition
language which has been developed to describe abstractly the values
protocol data units can assume; this is of considerable interest for
model checking as ASN.1 can be used to constrain/construct the state
space of the protocol accurately. However, with current practice, any
change to the English description cannot easily be checked for
consistency while protocols are being developed. In this work, we
have developed a SPIN-based tool called EASN (Enhanced ASN.1) where
the behaviour can be formally specified through a language based upon
Promela for control structures but with data models from ASN.1. An
attempt is also made to use international standards (for example,
X/Open std on ASN.1/C++ translation) as available so that the tool can
be realised with pluggable components. We have used EASN to validate a
simplified RLC in the 3G GSM stack that uses less memory than SPIN due
to the use of the subtyping information in the state compaction
infrastructure for EASN. In this short paper, we discuss the EASN
language, the architecture of the verification tool for EASN along
with an example usage.
