Abstract
The main limitation of software model checking is that, due to state explosion, it does not scale to real-world multi-threaded programs. One of the reasons is that current software model checkers adhere to full semantics of programming languages, which are based on very permissive models of concurrency. Current runtime platforms for programs, however, restrict concurrency in various ways — it is visible especially in the case of critical embedded systems, which typically involve only a single processor and use a threading model based on limited preemption.
In this paper, we present a technique for addressing state explosion in model checking of Java programs for embedded systems, which exploits restrictions on concurrency common to current Java platforms for such systems. We have implemented the technique in Java PathFinder and performed a number of experiments on Purdue Collision Detector, which is a non-trivial multi-threaded Java program. Results of experiments show that use of the restrictions on concurrency in model checking with Java PathFinder reduces the state space size by an order of magnitude and also reduces the time needed to discover errors in Java programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andreae, C., Coady, Y., Gibbs, C., Noble, J., Vitek, J., Zhao, T.: Scoped Types and Aspects for Real-Time Java. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 124–147. Springer, Heidelberg (2006)
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A Model Checker for Concurrent Software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)
Armbuster, A., Baker, J., Cunei, A., Flack, C., Holmes, D., Pizlo, F., Pla, E., Prochazka, M., Vitek, J.: A Real-Time Java Virtual Machine for Avionics. ACM Transactions on Embedded Computing Systems 7(1) (2007)
Bollella, G., Gosling, J., Brosgol, B., Dibble, P., Furr, S., Turnbull, M.: The Real-Time Specification for Java. Java Series. Addison-Wesley, Reading (2000)
CLDC HotSpot Implementation Virtual Machine, White Paper, Sun Microsystems, http://java.sun.com/products/cldc/wp/CLDC_HI_WhitePaper.pdf (accessed in March 2009)
De, A., Roychoudhury, A., D’Souza, D.: Java Memory Model aware Software Validation. In: Proceedings of the 8th ACM Workshop on Program Analysis for Software Tools and Engineering (PASTE 2008). ACM Press, New York (2008)
Dwyer, M.B., Hatcliff, J., Hoosier, M., Robby: 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.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)
Groce, A., Visser, W.: Heuristics for Model Checking Java Programs. International Journal on Software Tools for Technology Transfer 6(4) (2004)
Huynh, T.Q., Roychoudhury, A.: A Memory Model Sensitive Checker for C#. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 476–491. Springer, Heidelberg (2006)
IBM J9 Java Virtual Machine, http://wiki.eclipse.org/index.php/J9 (accessed March 2009)
Iosif, R.: Symmetry Reductions for Model Checking of Concurrent Dynamic Software. International Journal on Software Tools for Technology Transfer (STTT) 6(4) (2004)
Jikes RVM (Research Virtual Machine), http://jikesrvm.org (accessed in March 2009)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Prentice Hall, Englewood Cliffs (1999)
Musuvathi, M., Qadeer, S.: Iterative Context Bounding for Systematic Testing of Multithreaded Programs. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2007). ACM Press, New York (2007)
Pelanek, R.: Fighting State Space Explosion: Review and Evaluation. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 37–52. Springer, Heidelberg (2009)
Pizlo, F., Fox, J., Holmes, D., Vitek, J.: Real-time Java Scoped Memory: Design patterns and Semantics. In: Proceedings of the 7th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2004). IEEE CS, Los Alamitos (2004)
Qadeer, S., Rehof, J.: Context-Bounded Model Checking of Concurrent Software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)
Rabinovitz, I., Grumberg, O.: Bounded Model Checking of Concurrent Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82–97. Springer, Heidelberg (2005)
The Scala Programming Language, http://www.scala-lang.org/ (accessed in March 2009)
Srinivasan, S., Mycroft, A.: Kilim: Isolation-Typed Actors for Java. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 104–128. Springer, Heidelberg (2008)
Sun Java SE HotSpot, Sun Microsystems, http://java.sun.com/javase/technologies/hotspot/ (accessed in March 2009)
Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. Automated Software Engineering Journal 10(2) (2003)
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenstrom, P.: The Worst-Case Execution-Time Problem - Overview of Methods and Survey of Tools. ACM Transactions on Embedded Computing Systems 7(3) (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Parizek, P., Kalibera, T. (2009). Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs. In: Alpuente, M., Cook, B., Joubert, C. (eds) Formal Methods for Industrial Critical Systems. FMICS 2009. Lecture Notes in Computer Science, vol 5825. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04570-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-04570-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04569-1
Online ISBN: 978-3-642-04570-7
eBook Packages: Computer ScienceComputer Science (R0)