Parizek, Pavel and Kalibera, Tomas (2009) Platform-specific restrictions on concurrency in model checking of Java programs. In: Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS).
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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.
|Item Type:||Conference or workshop item (UNSPECIFIED)|
|Uncontrolled keywords:||determinacy analysis, Craig interpolants|
|Subjects:||Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,|
|Divisions:||Faculties > Science Technology and Medical Studies > School of Computing|
|Depositing User:||Tomas Kalibera|
|Date Deposited:||21 Sep 2012 09:49|
|Last Modified:||21 Sep 2012 09:49|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/30583 (The current URI for this page, for reference purposes)|
- Depositors only (login required):