Towards Model Checking of Network Applications for IoT System Development

Abstract

With the expansion of the Internet, Internet of Things (IoT) gains lots of interest from industries and academia. IoT applications enable human-to-device and device-to-device interactions. For a successful deployment of IoT systems and services, software reliability is a very important requirement for IoT to ensure that data/messages have been received and performed properly in a timely manner. The concurrent connections of embedded sensors and actuators are nondeterministic in nature which makes testing insufficient to guarantee program correctness. In contrast, model checking techniques explore the entire behavior of a system under test (SUT) in brute-force and systematic manner. It investigates each reachable state for different thread schedules. Recent model checking techniques have been applied directly to networked programs. This paper reviews model checking techniques for networked applications and presents their strengths and limitations. A preliminary proposal for model checking of networked applications that addresses the identified gap is presented.