Extending JPF to verify distributed systems
- 11 February 2014
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGSOFT Software Engineering Notes
- Vol. 39 (1), 1-5
- https://doi.org/10.1145/2557833.2560577
Abstract
This paper presents our work on model checking distributed applications. We refer to distributed applications as a collection of communicating processes, regardless of their physical locations and the communication means. Our work targets applications written in Java. It relies on the multiprocess support included in Java Pathfinder (JPF) version 7 which allow for verifying the bytecode of distributed applications. The basic support for distributed applications in JPF does not account for communication between processes. In this work, we address this limitation. The work is implemented as a JPF extension which models inter- process communication (IPC) mechanisms. It uses a form of partial order reduction (POR) to explore all possible executions of a distributed Java application. Moreover, our approach provides a functionality to check the given distributed application against possible network failures which can occur at the operating system or the hardware layer.This publication has 3 references indexed in Scilit:
- Modeling class loaders in Java PathFinder version 7ACM SIGSOFT Software Engineering Notes, 2012
- NetstubPublished by Association for Computing Machinery (ACM) ,2007
- Accurate Centralization for Applying Model Checking on Networked ApplicationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006