EASN: Integrating ASN.1 and Model Checking

Telecommunication protocol standards have in the past and typically still use both an English description of the protocol and an ASN.1[5] specification of the data-model. 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 behavior can be formally specified through a language based upon Promela for control structures but with data models from ASN.1.We use the X/Open standard on ASN.1/C++ translation so that our tool can be realised with pluggable components.We have used EASN to validate a simplified RLC in the W-CDMA (3G GSM) stack. In this short paper1, we discuss the EASN language, the tool, and an example usage.