Multi-valued Model Checking A Smart Glucose Monitoring System with Trust

IoT in the e-Healthcare domain has recently seen much interest. The IoT applications in this domain involve extensive interactions between many components within open environments, making verifying these applications a significant challenge. This paper introduces a new framework for modelling and verifying IoT applications in the healthcare domain using a practical system verification technique called multi-valued model checking. We focus on applications that involve interactions based on trust protocols under inconsistency. Specifically, we introduce a new logic of trust called (4v-TCTL) to reason about the inconsistency between designers over IoT systems. We use a Smart Glucose Monitoring System as a case study. We model our system and assign six trust properties to be checked against this system. We introduce a new reduction algorithm for reducing our four-valued model checking problem to the two-valued version to reuse an existing model checker called MCMASt. We verified our system using our approach and reported the experimental results.