Sciweavers

Share
FMICS
2009
Springer

Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs

10 years 3 months ago
Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs
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...
Pavel Parizek, Tomás Kalibera
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2009
Where FMICS
Authors Pavel Parizek, Tomás Kalibera
Comments (0)
books