Argos is an imperative synchronous language with verification support.
To run Argos:
ArgoUML (version 8.1a)
Argos and Argonaute website