Timed HLPSL for specification and verification of time sensitive protocols