Abstract
Most applications today communicate with other processes over a network. Such applications are often multi-threaded. The non-determinism in the thread and communication schedules makes it desirable to model check such applications. When model checking such a networked application, a simple state space exploration scheme is not applicable, as the process being model checked would repeat communication operations when revisiting a given state after backtracking. We propose a solution that encapsulates such operations in a caching layer that is capable of hiding redundant communication operations from the environment. This approach is both more portable and more scalable than other approaches, as only a single process executes inside the model checker.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Artho, C., Garoche, P.: Accurate centralization for applying model checking on networked applications. In: Proc. 21st Intl. Conf. on Automated Software Engineering (ASE 2006), Tokyo, Japan, pp. 177–188. IEEE Computer Society (2006)
Artho, C., Schuppan, V., Biere, A., Eugster, P., Baur, M., Zweimüller, B.: JNuke: Efficient Dynamic Analysis for Java. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 462–465. Springer, Heidelberg (2004)
Artho, C., Sommer, C., Honiden, S.: Model checking networked programs in the presence of transmission failures. In: Proc. 1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007), Shanghai, China, pp. 219–228. IEEE Computer Society (2007)
Artho, C., Zweimüller, B., Biere, A., Shibayama, E., Honiden, S.: Efficient model checking of applications with input/output. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol. 4739, pp. 515–522. Springer, Heidelberg (2007)
Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstractions for Model Checking C Programs. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 268–285. Springer, Heidelberg (2001)
Barlas, E., Bultan, T.: Netstub: a framework for verification of distributed Java applications. In: Proc. 22nd Intl. Conf. on Automated Software Engineering (ASE 2007), Atlanta, USA, pp. 24–33. ACM (2007)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Transactions on Software Engineering 30(6), 388–402 (2004)
Chandra, S., Godefroid, P., Palm, C.: Software model checking in practice: an industrial case study. In: Proc. 24th Intl. Conf. on Software Engineering (ICSE 2002), pp. 431–441. ACM Press, New York (2002)
Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C.: Bandera: Extracting finite-state models from Java source code. In: Proc. 22nd Intl. Conf. on Software Engineering (ICSE 2000), Limerick, Ireland, pp. 439–448. ACM Press (2000)
Dingel, J.: Computer-assisted assume/guarantee reasoning with VeriSoft. In: Proc. 25th Intl. Conf. on Software Engineering (ICSE 2003), Washington, USA, pp. 138–148. IEEE Computer Society (2003)
Dwyer, M., Hatcliff, J., Hoosier, M.: Building your own software model checker using the Bogor extensible model checking framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 148–152. Springer, Heidelberg (2005)
Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proc. 24th ACM Symposium on Principles of Programming Languages (POPL 1997), Paris, France, pp. 174–186. ACM Press (1997)
Goldberg, I., Wagner, D., Thomas, R., Brewer, E.: A secure environment for untrusted helper applications. In: Proc. 6th Usenix Security Symposium (SSYM 1996), San Jose, USA, pp. 1–13. USENIX Association (1996)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley (2005)
Musuvathi, M., Park, D., Chou, A., Engler, D., Dill, D.: CMC: a pragmatic approach to model checking real code. SIGOPS Oper. Syst. Rev. 36(SI), 75–88 (2002)
Nakagawa, Y., Potter, R., Yamamoto, M., Hagiya, M., Kato, K.: In: Proc. Workshop on Dependable Software: Tools and Methods, Yokohama, Japan, pp. 215–220 (2005)
Paredes, S.: Jget (2006), http://www.cec.uchile.cl/~sparedes/jget/
Stoller, S., Liu, Y.: Transformations for model checking distributed Java programs. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 192–199. Springer, Heidelberg (2001)
Sun Microsystems, Santa Clara, USA. A simple, multi-threaded HTTP server (2008), http://www.java.sun.com/developer/technicalArticles/Networking/Webserver/
Tanenbaum, A.: Modern operating systems. Prentice-Hall (1992)
Tanenbaum, A.: Computer Networks. Prentice-Hall (2002)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal 10(2), 203–232 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Artho, C., Leungwattanakit, W., Hagiya, M., Tanabe, Y. (2008). Efficient Model Checking of Networked Applications. In: Paige, R.F., Meyer, B. (eds) Objects, Components, Models and Patterns. TOOLS EUROPE 2008. Lecture Notes in Business Information Processing, vol 11. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69824-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-69824-1_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69823-4
Online ISBN: 978-3-540-69824-1
eBook Packages: Computer ScienceComputer Science (R0)