Extending a Component Specification Language with Time

In a formal approach to component specification, interfaces are usually described using pre- and postconditions of methods or protocols. In this paper we present an approach for integrating time into a component specification language which already allows for pre/post and protocol descriptions. The specification of timing aspects is indispensable when treating components of embedded systems underlying hard real-time requirements. In order to allow for a smooth integration into the existing specification language and to ease reading and writing of interfaces, we do not extend the language with yet another formalism (for time), but instead only add a specific feature (i.e. clocks) to it. We define a semantics for this new specification language in terms of timed automata, which thus also opens the possibility of analysing interface descriptions with the UPPAAL model checker. We furthermore give timed simulation conditions and prove their soundness with respect to inclusion of timed traces, the notion of implementation in timed automata. This implementation relation can be used as a correctness criterion for interoperability and substitutability checks.