Treffer: Software Model Checking for Distributed Applications using Hybridization of Centralization and Cache Approaches.

Developing reliable distributed systems poses significant challenges due to the nondeterministic nature of thread and process execution, as well as communication channels. Software model checking offers a means to verify system correctness by exhaustively analyzing all program execution paths. However, the existing bytecode model checker, capable of verifying multiple processes, suffers from computational overhead. This paper introduces Java PathFinder (JPF)-Nas-Hybrid (JNH), a novel model checker addressing these limitations. JNH employs a redesigned inter-process communication (IPC) model and integrates a scalable caching mechanism. The experimental results show that the hybridization of centralization with cache significantly reduces the computational overhead and improves verification performance as well. Additionally, the paper explores bug detection strategies, distinguishing between local and global bugs, and evaluates various search strategies to explore distributed program state spaces. In every case, the proposed method results in a smaller state space, fewer bytecode instructions, and a shallower search graph. [ABSTRACT FROM AUTHOR]

Membangunkan sistem teragih yang boleh dipercayai menimbulkan cabaran yang ketara disebabkan oleh sifat bukan penentu bagi pelaksanaan thread dan proses, serta saluran komunikasi. Pemeriksaan model perisian menawarkan cara untuk mengesahkan ketepatan sistem dengan menganalisis secara menyeluruh semua laluan pelaksanaan program. Walau bagaimanapun, penyemak model kod bait sedia ada, yang mampu mengesahkan pelbagai proses, mengalami overhed pengiraan. Artikel ini memperkenalkan Java PathFinder (JPF)- Nas-Hybrid (JNH), penyemak model baru yang menangani batasan ini. JNH menggunakan model komunikasi antara proses (IPC) yang direka bentuk semula dan menyepadukan mekanisme caching berskala. Keputusan eksperimen menunjukkan bahawa penghibridan pemusatan dengan cache dengan ketara mengurangkan overhed pengiraan dan juga meningkatkan prestasi pengesahan. Selain itu, artikel ini meneroka strategi pengesanan pepijat, membezakan antara pepijat tempatan dan global, dan menilai pelbagai strategi carian untuk meneroka ruang keadaan program yang diedarkan. Dalam setiap kes, kaedah yang dicadangkan menghasilkan ruang keadaan yang lebih kecil, arahan kod bait yang lebih sedikit dan graf carian yang lebih cetek. [ABSTRACT FROM AUTHOR]

Copyright of Asia-Pacific Journal of Information Technology & Multimedia is the property of Asia-Pacific Journal of Information Technology & Multimedia and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)