Using TILCO for specifying real-time systems