Specification and Analysis of Timed and Functional TRMCS Behaviours