Abstract
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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Holzmann Gerald J., Doron Peled, ‘The state of SPIN’, CAV’ 96.
Shanbhag Vivek K., K. Gopinath, ‘A Spin based model checker for telecommunication protocols’, May 2001, 8th Intl SPIN Workshop on Model Checking of Software.
G. Gerth, D. Peled, M. Y. Vardi, P. Wolper, ‘Simple On-the-fly Automatic Verification of Linear Temporal Logic’, PSTV94.
Holzmann, G.J., Design and Validation of Computer Protocols, Prentice Hall, 1992.
Holzmann, G.J., SPIN Sources, Version 3.4.6, 29th March. 2001.
J. Geldenhuys, PJA de Villiers, ‘Runtime Efficient State Compaction in SPIN’, 5th Intl SPIN Workshop on Theoretical Aspects of Model Checking, ed. D. Dams, M. Massnik.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shanbhag, V.K., Gopinath, K., Turunen, M., Ahtiainen, A., Luukkainen, M. (2001). EASN: Integrating ASN.1 and Model Checking. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_37
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_37
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive