Abstract. Specifying the correctness of complex concurrent and realtime systems is a crucial problem. Many property languages have been proposed to do so; however, these techniques often involve formalisms not easily handled by engineers, and furthermore require dedicated tools. We propose here a set of patterns that encode common specification or verification components when dealing with concurrent real-time systems. We provide a formal semantics for these patterns, as time Petri nets, and show that they can encode previous approaches.