This paper presents the modelisation of a special class of timed automata, named p-automata in the proof assistant Coq. This work was performed in the framework of the CALIFE project¹ which aims to build a general platform for specification, validation and test of critical algorithms involved in telecommunications. This paper does not contain new theoretical results but explains how to combine and adapt known techniques in order to build an environment dedicated to a class of problems. It emphasizes the specific features of Coq which have been used, in particular dependent types and tactics based on computational reflection.