Abstract. We describe a translation from a dialect of SDL-88 to PROMELA, the input language of the SPIN model checker. The fairly straightforward translation covers data types as well as processes, procedures, and services. Together with SPIN the translation provides a simulation and verification environment for most SDL features.