Formal Modeling and GDPR-Aware Design for Internet of Medical Things Systems
Internet of Medical Things (IoMT) systems involve many interconnected devices that continuously collect, process, and share sensitive health data, creating significant privacy risks. Ensuring that these systems comply with GDPR is particularly challenging because legal requirements are complex, often timedependent, and difficult to validate at the level of individual data operations. This paper addresses this challenge by proposing a new formal verification approach that models the main IoMT operations, including data collection, transfer, storage, processing, and automated decision-making, as a GDPR-aware timed automaton. The proposed approach encodes legal requirements as formal rules and verifies compliance using a model checker through safety, liveness, and reachability properties. A remote cardiac monitoring scenario is presented to demonstrate typical data flows and interactions among smart medical devices, with business process models to represent the system. Experimental results show that the approach remains efficient as system complexity increases, providing a practical solution for developing IoMT applications that integrate privacy-by-design principles from the outset.