Αποστολή με SMS: Specification and proof in real-time CPS