This paper presents the formal modeling and performance analysis of one of Internet of Things (IoT) protocols. The Internet of Things is among the subjects best financed in the industry and studied in the academic world. The rapid evolution of mobile Internet, the manufacture of mini hardware, microcomputer, and machine-to-machine (M2M) enabled IoT technologies to be at the top of media subjects. These technologies allow things or devices that are not computers to act intelligently and to make collaborative decisions that are beneficial for certain applications. Hence, the intelligent decision making, the self configuration and the ad hoc networking are from the main characteristics of IoT. Therefore, the implementation of protocols for IoT must comply the standards and satisfy the good properties. Using formal methods in the study of developed protocols ensure these conditions. In this paper, we use probabilistic timed automata for the formal modeling of Message Queue Telemetry Transport (MQTT) and we use further statistical model checking of UPPAAL SMC tool-set for the performance evaluation of the protocol.

In reconfigurable manufacturing systems (RMSs), the structure of the system can be changed during its execution. This reconfiguration can be triggered by several motivations: a new requirement in the production process, avoiding some problems caused by machines breakdowns, etc. RMSs are characterised by their flexibility which guarantees productivity and efficiency. However, their design is more complicated and needs new techniques and paradigms. The use of high level Petri nets (PNs) offers the ability to design these systems and to analyse their properties. In this article, the authors apply reconfigurable object nets (RONs) for the modelling, simulation and analysis of RMSs. Indeed, a formal method is proposed, where the reconfiguration process is specified explicitly as a graph transformation, the simulation is realised using the RON-tool, and the analysis exploits the TINA-tool (timed nets analyser tool).