AbstractMachine-to-Machine communications (M2M) is emerging as a new technology for next generation of communicating systems. In such M2M based systems, a large number of intelligent machines share information and make collaborative decisions without human interventions. M2M is involved in several fields and in particular, in critical ones such as the healthcare services, where requirements in term of Quality of Services (QoS) and particularly time related requirements must be thoroughly enforced. In this paper, we are interested in the verification problem of Publish/Subscribe based M2M systems where we consider time related requirements. In this context, we first characterize Publish/Subscribe communications on the top of the OM2M platform, which is an implementation of the ETSI M2M standard. Then, we introduce a formal graph based model to specify Publish/Subscribe communications associated to time related requirements. Based on the defined formal model, we provide a model checking based techniques to validate time requirements for data exchange delays.