Temporal verification of mobile publish/subscribe machine-to-machine communications

With the proliferation of data, components and services on the internet, cyber-physical systems are growing up these last years. Machine-to-Machine (M2M) is an example of a cyber-physical system where mobile communication is enabled between sensors, gateways and application services. M2M is used in several domains and in particular, in critical ones such as the healthcare domain. In such domain, requirements in term of Quality of Service (QoS) and particularly time related requirements in mobile environments must be rigorously respected. It is important to define an approach to ensure and validate these systems against these requirements. In this paper, we are interested in Publish/ Subscribe M2M communication based model. Our goal is to define a formal approach that aims at designing and validating M2M systems where we consider M2M mobile sensors and time related requirements. We define a graph based model to characterize Publish/ Subscribe M2M systems and model checking mechanisms to enable verification techniques.