On the Specification and Verification of Performance Properties for a Timed Process Algebras