Towards Model Checking of Network Applications for IoT System Development

Hing Ratana, Sharifah Mashita Syed Mohamad


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.


Cache-Based Approach; Internet of Things Applications; Network Model Checking; Software Reliability;

Full Text:



T. Priestley, “The internet of things is a fragmented $19 trillion roulette gamble,” Forbes, 2015. Available at sites/theopriestley/2015/10/05/the-internet-of-things-is-a-fragmented- 19-trillion-roulette-gamble/#6f7c579d29d9. [Accessed: 28-Feb-2017].

B. L. Risteska Stojkoska and K. V. Trivodaliev, “A review of Internet of Things for smart home: challenges and solutions,” J. Clean. Prod., vol. 140, pp. 1454–1464, Jan. 2017.

I. Lee and K. Lee, “The Internet of Things (IoT): Applications, investments, and challenges for enterprises,” Bus. Horiz., vol. 58, no. 4, pp. 431–440, Jul. 2015.

C. Baier and J.-P. Katoen, Principles of Model Checking. The MIT Press, Cambridge, 2008.

E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. The MIT Press, Cambridge, 1999.

W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto, and K. Takahashi, “Modular software model checking for distributed systems,” IEEE Trans. Softw. Eng., vol. 40, no. 5, pp. 483–501, May 2014.

N. Shafiei, and P. Mehlitz, “Extending JPF to verify distributed systems,” ACM SIGSOFT Softw. Eng. Notes, vol. 39, no. 1, pp. 1–5, Feb. 2014.

N. Sebih, F. Weitl, C. Artho, M. Hagiya, Y. Tanabe, and M. Yamamoto, “Software model checking of udp-based distributed applications,” in 2014 Second International Symposium on Computing and Networking, 2014, pp. 96–105.

E. M. Clarke, “The birth of model checking,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2008, vol. 5000 LNCS, pp. 1–26.

P. Godefroid, “Model checking for programming languages using verisoft,” in Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997, pp. 174– 186.

J. C. Corbett et al., “Bandera: extracting finite-state models from java source code,” in Proceedings of the 22Nd International Conference on Software Engineering, 2000, pp. 439–448.

T. Ball, A. Podelski, and S. K. Rajamani, “Boolean and cartesian abstraction for model checking C programs,” in Tools and Algorithms for the Construction and Analysis of Systems, T. Margaria, and W. Yi, Eds. Berlin, Heidelberg: Springer, 2001, pp. 268–283.

T. Ball and S. K. Rajamani, “The SLAM toolkit,” in Computer Aided Verification, G. Berry, H. Comon, and A. Finkel, Eds. Berlin, Heidelberg: Springer, 2001, pp. 260–264.

W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda, “Model checking programs,” Autom. Softw. Eng., vol. 10, no. 2, pp. 203–232, 2003.

S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith, “Modular Verification of software components in C,” in Proceedings of the 25th International Conference on Software Engineering, 2003, pp. 385–395.

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Software verification with BLAST,” in Model Checking Software, T. Ball and S. K. Rajamani, Eds. Berlin, Heidelberg: Springer, 2003, pp. 235–239.

C. Artho, C. Artho, A. Biere, P. Eugster, M. Baur, and B. Zweimüller, “JNuke: efficient dynamic analysis for Java,” in Proc. CAV ’04, pp. 462-465, 2004.

M. B. Dwyer, J. Hatcliff, M. Hoosier, and Robby, “Building your own software model checker using the bogor extensible model checking framework,” in Computer Aided Verification, K. Etessami and S. K. Rajamani, Eds. Berlin, Heidelberg: Springer, 2005, pp. 148–152.

C. Artho, B. Zweimüller, A. Biere, E. Shibayama, and S. Honiden, “Efficient model checking of applications with input/output,” in Computer Aided Systems Theory, R. Moreno-D’iaz, F. Pichler, and A. Quesada-Arencibia, Eds. Berlin, Heidelberg: Springer, 2007, pp. 515– 522.

C. Artho, W. Leungwattanakit, M. Hagiya, and Y. Tanabe, “Efficient model checking of networked applications,” in 46th International Conference Objects, Components, Models and Patterns Proceedings, 2008, vol. 11, pp. 22–40.

C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe, and M. Yamamoto, “Cache-based model checking of networked applications: from linear to branching time,” in 24th {IEEE/ACM} International Conference on Automated Software Engineering, Auckland, New Zealand, 2009, pp. 447–458.

W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, and M. Yamamoto, “Model checking distributed systems by combining caching and process checkpointing,” in 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), 2011, pp. 103–112.

S. D. Stoller and Y. A. Liu, “Transformations for model checking distributed Java programs,” in SPIN ’01: Proceedings of the 8th international SPIN workshop on Model checking of software, 2001.

C. Artho and P.-L. Garoche, “Accurate centralization for applying model checking on networked applications,” in 21st IEEE/ACM International Conference on Automated Software Engineering (ASE’06), 2006, pp. 177–188.

E. Barlas and T. Bultan, “Netstub: a framework for verification of distributed Java applications,” in Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering, 2007, pp. 24–33.

Y. Nakagawa, R. Potter, M. Yamamoto, M. Hagiya, and K. Kato, “Model checking of multi-process applications using SBUML and GDB,” in Proc. Workshop on Dependable Software: Tools and Methods, 2005, pp. 215–220.

L. Ma, C. Artho, and H. Sato, “Analyzing distributed Java applications by automatic centralization,” in 2013 IEEE 37th Annual Computer Software and Applications Conference Workshops, 2013, pp. 691–696.

J. Ansel, K. Arya, and G. Cooperman, “DMTCP: Transparent checkpointing for cluster computations and the desktop,” in 2009 IEEE International Symposium on Parallel & Distributed Processing, 2009, pp. 1–12.


  • There are currently no refbacks.

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.

ISSN: 2180-1843

eISSN: 2289-8131