{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:20:06Z","timestamp":1750306806833,"version":"3.41.0"},"reference-count":6,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,11]],"date-time":"2014-02-11T00:00:00Z","timestamp":1392076800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2014,2,11]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/2557833.2560577","type":"journal-article","created":{"date-parts":[[2014,2,18]],"date-time":"2014-02-18T14:08:32Z","timestamp":1392732512000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Extending JPF to verify distributed systems"],"prefix":"10.1145","volume":"39","author":[{"given":"Nastaran","family":"Shafiei","sequence":"first","affiliation":[{"name":"NASA Ames Research Center, Moffett Field, California"}]},{"given":"Peter","family":"Mehlitz","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center, Moffett Field, California"}]}],"member":"320","published-online":{"date-parts":[[2014,2,11]]},"reference":[{"volume-title":"Springer-Verlag","year":"2010","author":"Pitt Esmond","key":"e_1_2_1_1_1"},{"volume-title":"SPIN","year":"2001","author":"Scott","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2006.10"},{"volume-title":"Proceedings of Workshop on Dependable Software: Tools and Methods","year":"2005","author":"Nakagawa Yoshihito","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321638"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382756.2382800"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560577","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2557833.2560577","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:58Z","timestamp":1750232098000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560577"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,11]]},"references-count":6,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2,11]]}},"alternative-id":["10.1145\/2557833.2560577"],"URL":"https:\/\/doi.org\/10.1145\/2557833.2560577","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2014,2,11]]},"assertion":[{"value":"2014-02-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}