### Towards Model Checking of Network Applications for IoT System Development

#### Abstract

#### Keywords

#### Full Text:

PDF#### References

T. Priestley, “The internet of things is a fragmented $19 trillion roulette gamble,” Forbes, 2015. Available at https://www.forbes.com/ 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.

### Refbacks

- There are currently no refbacks.

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

**ISSN: 2180****-1843**

*eISSN:* **2289-8131**