A SPIN-based model checker for telecommunication protocols

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 and SDL model) and an ASN.1 specification of the data-model, thus likely making the specification incomplete. ASN.1 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 subtyping in 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 (X/Open std on ASN.1/C++ translation) as available so that the tool can be realised with pluggable components. One major design criterion is to enable incremental computation wherever possible (for example: hash values, consistency between alternate representations of state). We have used EASN to validate a simplified model of RLC (Radio Link Control) in the W-CDMA stack that imports data types from its associated ASN.1 model. In this paper, we discuss the motivation and design of the EASN language, the architecture and implementation of the verification tool for EASN and some preliminary performance indicators.

References

1. 1.Holzmann, Gerald J., Doron Peled, "The state of SPIN", CAV '96.]]
2. 2.Rob Gerth, Eindhoven University, "Concise Promela Reference", August 1997, Soft-copy available with SPIN.]]
3. 3.G. Gerth, D. Peled, M. Y. Vardi, P. Wolper, "Simple On-the- y Automatic Verification of Linear Temporal Logic", PSTV94.]]
4. 4.Holzmann, G.J., Design and Validation of Computer Protocols, Prentice Hall, 1992.]]
5. 5.Patrice Godefroid, "Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem", PhD Thesis, University of Liege, Computer Science Department, Nov. '94.]]
6. 6.Information Technology - Abstract Syntax Notation One (ASN.1): Specification of Basic Notation, (Technical Corr. 1, Amd. 1:Rules of extensibility), ITU-T Rec. X.680 (1994), Corr.1 (1995), Amd. 1 (1995); Information Object Specification (Amd. 1: Rules of Extensibility), ITU-T Rec. X.681 (1994), Amd. 1 (1995); Constraint Specification, ITU-T Rec. X.682 (1994); Parameterization of ASN.1 specifications, ITU-T Rec. X.683 (1994)]]
7. 7.ASN.1/C++ Application Programming Interface, Part 1: Base Classes & Specifific Interface, & Part 2: Generic Interface, NMF 040- 1 & 2,Issue 1.0, Feb. 1998]]
8. 8.Holzmann, G.J., SPIN Sources, Version 3.4.1, 15th August 2000; "Basic Spin Manual", available with SPIN.]]
9. 9.J.Geldenhuys, PJA de Villiers, Runtime Efficient State Compaction in SPIN,' The 5th Intl SPIN Workshop on Theoretical Aspects of Model Checking.]]
10. 10.Anindya Basu, A Language-based Approach to Protocol Construction', PhD Dissertation, Cornell Univ., Aug. '97]]
11. 11.ASN.1/C++ Application Programming Interface, Issue 1.0 Draft 10a - Submission to X/Open August 21, 1996]]
12. 12.Appendix A: The ASN.1 language, and Appendix B:The EASN Language, are only in the full paper; available at http://144.16.67.13/~ gopi/spin01/easn.ps.gz.]]

• Software and its engineering

  • Software organization and properties

    • Software functional properties

      • Formal methods