Multi-valued verification of commitment systems with uncertainty and inconsistency in multi-source data settings

In the dynamic landscape of Internet of Things (IoT) applications within multi-source data environments, ensuring the reliability and correctness of system communications has become a paramount concern. This is particularly evident in the presence of commitment protocols with inconsistency and uncertainty. This paper tackles these challenges by introducing a new logic, termed Six-Values Computation Tree Logic for Commitment (6V-CTLC), specifically crafted to adeptly model IoT systems with both inconsistency and uncertainty. Employing this logic, we devise an innovative reduction-based multi-valued model checking approach to verify the systems under scrutiny. Our method is implemented through a Java transformation tool we developed to translate the 6V-CTLC logic to the classical logic of commitment (CTLC) and seamlessly interfaces with the efficient model checker MCMAS+. Applying this approach, we verify an abstracted 6V-CTLC model featuring uncertainty and inconsistency, as well as the original model of our system before abstraction. Furthermore, we assess the scalability of our approach through ten experiments, comparing the results obtained from verifying the two models. The findings demonstrate the effectiveness of system abstraction in mitigating the state explosion problem, while the developed multi-valued model checking technique yields precise results.