SMS versenden: Formálna verifikácia zjemnenej špecifikácie v jazyku HSSL