Toward Secure and Reliable IoT Systems: A Comprehensive Review of Formal Methods Applications

Abstract

The exponential growth of Internet of Things (IoT) applications poses substantial obstacles in guaranteeing their dependability, safety, and effectiveness. Formal methods provide precise mathematical techniques for modeling, verifying, and analyzing these systems, effectively addressing important aspects of their creation and implementation. This review provides a thorough examination of the utilization of formal methods in the field of IoT, focusing on recent research published in well- regarded academic journals and conferences. We examine different formal methodologies, such as temporal logic, automata theory, theorem proving, and formal specification languages, emphasizing their efficacy in tackling difficulties peculiar to IoT systems. The review assesses the benefits and constraints of these methodologies, contrasts various approaches, and integrates essential discoveries. Key contributions include a comprehensive overview of formal methods applications, identification of critical challenges, evaluation of the effectiveness of different techniques, and proposals for future research directions. By highlighting emerging trends and future research paths, this review underscores the significance of formal approaches in enhancing the safety and resilience of IoT systems. This review seeks to serve as a beneficial reference for researchers and practitioners looking to improve IoT applications through formal verification and analysis techniques.

Keywords

• Formal methods
• Internet of Things (IoT)
• reliability in IoT
• model checking
• theorem proving
• formal specification