Specification and analysis of hardware systems using timed process algebras

The ability of unambiguously specifying (in a mathematical sense) and rigorously analysing timing properties/constraints is fundamental to design correct hardware systems. Formalisms in which hardware behaviour and timing properties can be precisely captured is a mandatory prerequisite for designing correct hardware systems (discrete-time systems by nature). Timed process algebras are such formalisms. To show that timed process algebras are useful for formal specification and analysis of hardware systems, in this paper, we illustrate the use of a timed process algebra called timed Chi (X) with several benchmark examples of hardware systems.