We propose some mild modifications to the syntax and semantics of Timed CSP which significantly increase expressiveness. As a result, we are able to capture some of the most widely used specifications on timed systems as refinements (reverse inclusion of sets of behaviours) which may then be verified using the model checker FDR. We characterize the expressive power of the finite-state fragment of this augmented version of Timed CSP as that of closed timed epsilon-automata -- timed automata with epsilon-transitions (silent transitions) and closed invariant and enabling clock constraints.
Nordic Journal of Computing 10, 2003. 35 pages.
PostScript / PDF
© 2003 Nordic Journal of Computing.