Yasushi Kodama

Yasushi Kodama


Research Focus & Metrics

Academic Career Length

4Years (2023-Present)

(Calculated once Scilit publication data is synced: current year − year of first publication + 1)

Representative Publications

View All Publications

25 October 2024 in Electronics
Verified
Journal Article
Open access
PDF file
TKTsutomu Kumazawa
Tsutomu Kumazawa
Munehiro TakimotoMunehiro Takimoto
Munehiro Takimoto
YKYasushi Kodama
Yasushi Kodama
Yasushi KambayashiYasushi Kambayashi
Yasushi Kambayashi
In software engineering, errors or faults in software systems often lead to critical social problems. One effective methodology to tackle this problem is model checking, which is an automated formal verification technique. In traditional model checking, the task of finding specification errors is reduced to deterministic search techniques such as Depth-First Search. Recent research has shown that swarm intelligence offers a powerful search capability compared to traditional techniques. In particular, multi-swarm Particle Swarm Optimization is known to be efficient and can mitigate the state-space explosion problem, i.e., the exponential increase in the search space with a linear increase in the problem size. However, the state-space explosion problem is still significant when verifying very large systems. Further performance improvement is needed. To achieve this, we propose a novel memoization or cache mechanism for storing tentative solutions for reuse in the later stages of the search procedure. For each stage, a candidate solution computed by a swarm is summarized efficiently and heuristically to consolidate similar solutions into a single representative solution. We store the summary and its associated solutions in key-value maps. Instead of computing known solutions repeatedly, we retrieve the solution if the stored key matches the summary. We incorporated the proposed mechanism into a model-checking technique with multi-swarm Particle Swarm Optimization and evaluated the search performance. We show in this paper that the proposed mechanism improved time and space consumption while maintaining solution quality.

5 October 2025
Verified
Book Chapter
Closed access
PDF file
TKTsutomu Kumazawa
Tsutomu Kumazawa
Munehiro TakimotoMunehiro Takimoto
Munehiro Takimoto
YKYasushi Kodama
Yasushi Kodama
Yasushi KambayashiYasushi Kambayashi
Yasushi Kambayashi