© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Platform-specific restrictions on concurrency in model checking of Java programs
Pavel Parizek and Tomas Kalibera
In Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), pages 182-196. Springer, November 2009 [doi].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.
Download publication 159 kbytes (PDF)Bibtex Record
@inproceedings{3132,
author = {Pavel Parizek and Tomas Kalibera},
title = {Platform-specific restrictions on concurrency in model checking of {Java} programs},
month = {November},
year = {2009},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {10.1007/978-3-642-04570-7_10},
url = {http://www.cs.kent.ac.uk/pubs/2009/3132},
publication_type = {inproceedings},
submission_id = {1574_1308854377},
ISBN = {978-3-642-04569-1},
booktitle = {Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS)},
publisher = {Springer},
refereed = {yes},
}