EASN: Integrating ASN.1 and Model Checking

Vivek K. Shanbhag, K. Gopinath, Markku Turunen, Ari Ahtiainen, Matti Luukkainen

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

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.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems