大規模システムの膨大な「動作チェック」を小分けして高速に
―省メモリで検証できる新手法「DCA2MC」を開発―

【ポイント】

• 膨大な「動作チェック」を小さな問題に分け、複数の計算機で並列処理する新手法を開発しました。
• 既存の検証ツールが1テラバイトのメモリを使い切った一部の条件でも、検証を完了しました。
• 複雑なソフトウェアやハードウェアの不具合を、開発段階で見つけやすくすることが期待されます。

【概要】

１．背景

　現在の情報システムでは、多数の処理が同時に動き、互いに情報をやりとりしながら全体の処理を進めています。このようなシステムでは、それぞれの処理が実行される順番が少し変わるだけでも、システム全体の動作が変わることがあります。
　そのため、あらかじめ決めた条件だけを試す通常のテストでは、起こる得るすべての動作を確認し、不具合を見つけることは困難です。
　そこで利用されているのが「モデル検査」です。モデル検査は、ソフトウェアやハードウェアが取り得る動作を網羅的に調べ、求められる性質を満たしているかを自動的に確認する技術です。
　しかし、システムが大きく複雑になるほど、確認しなければならない状態や動作の組合せは急激に増えていきます。これは「状態空間爆発」と呼ばれ、計算機のメモリを使い切ったり、検査に非常に長い時間がかかったりする原因になります。大規模なシステムにモデル検査を適用するうえで、大きな課題の一つとなっていました。
　研究グループはこれまでにも、大きな検査問題をいくつかの小さな問題に分けて調べる「分割統治」の考え方をモデル検査に応用してきました。しかし、従来の方法では、調べたい性質の種類ごとに異なる理論や支援ツールが必要でした。
　そこで今回の研究では、論理式を一定の規則に従って分解する「タブロー法^*2」を、検査すべき範囲の分割に応用しました。これにより、「いつか起こる」「常に成り立つ」「ある条件が満たされたら、将来別の条件も満たされる」といったさまざまな性質を、一つの仕組みで扱えるようになりました。
　また、既存の並列モデル検査では、検査方法そのものを作り直す必要がある場合があります。DCA2MCでは、分割してできた小さな問題を既存のモデル検査ツールに渡して調べることができるため、既存ツールを大きく変更せずに利用できる点も特徴です。

２．研究内容
■膨大な「動作チェック」を小さな問題に分割

　本研究では、モデル検査の大きな問題を複数の小さな問題に分けて調べる手法「DCA2MC」を提案しました。
　モデル検査では、「ある状態が常に続く」「ある出来事が将来いつか起こる」といった、時間の流れに沿ったシステムの性質を表し、その性質が守られているかを調べます。
　本研究では、こうした性質を記述する線形時相論理（Linear Temporal Logic, LTL）^*3の式を、「タブロー法」の考え方を使って分解します（図1）。
　次に、その情報をもとに、システムの動きを調べる範囲を複数の層に分けます（図2）。層と層の境目では、「次に何を確かめる必要があるか」という条件を次の層へ引き継ぎながら、検証を進めます。
　こうして最終的にできた小さな検査問題は、それぞれ別々に処理することができます。そのため、一つの計算機で巨大な問題全体を一度に扱う必要がなくなり、使用するメモリを抑えることができます。
　さらに、それぞれの小さな問題は独立して処理できるため、複数の計算機を使って同時に検証することができ、検査時間の短縮につながります。
　ただし、大きな問題を小さく分けただけでは、元の問題と同じ正しい結論が得られるとは限りません。そこで研究グループは、分割後のすべての問題を調べることと、元の大きな問題を直接調べることが同じ結論になることを数学的に証明しました。
　この理論を形式仕様言語Maude上に実装したDCA2MCは、一つずつ問題を処理する逐次処理と、複数の問題を同時に処理する並列処理の両方に対応しています。また、問題の分け方を半自動的に選択する機能や、既存のモデル検査ツールSPINと連携する機能も備えています。
■1テラバイトのメモリでも完了できなかった検証を完了
　研究グループは、DCA2MCの有効性を確かめるため、複数の処理が同じ資源を同時に利用しないよう調整する5種類の「相互排他プロトコル^*4」（Qlock、Anderson、Ticket、MCS、TAS）を対象に検証実験を行いました。
　実験では、主に2種類の性質を調べました。一つは、「ある状態になった場合、その後いつか必ず別の状態になる」という性質（leads-to property）です。もう一つは、「ある状態が将来のどこかで少なくとも一度は実現する」という性質（eventual property）です。
　その結果、Qlockでは両方の性質について、またAndersonとTicketではleads-to propertyについて、既存の代表的なモデル検査ツールであるSPINとLTSminは、1テラバイトのメモリを使い切っても検証を完了できませんでした。
　一方、DCA2MCはこれらの検証を完了しました。
　さらに、分割してできた小さな検査問題を並列に処理することで、モデル検査の高速化も実現しました。

図1．タブロー法による線形時相論理式の分解
複雑な条件を枝分かれさせながら、より単純な条件へ分解していく様子を示しています。

図2．本アプローチによって分割された状態空間
システムが取り得る膨大な状態を複数の層に分け、それぞれを小さな検査問題として扱います。

３．社会への還元として期待できる内容、今後の展望

　今回の成果は、膨大な検査問題を適切に小分けすることで、これまで計算機のメモリや処理能力の制約から検証が難しかった大規模で複雑なシステムについても、検証できる可能性を広げるものです。
　一方で、似たような状態が多く現れる場合や、長い循環動作を含む場合には、問題を分割する効果が小さくなることがあります。そのため、DCA2MCがどのような場面でも既存のモデル検査ツールより高速になるわけではありません。
　今後は、似た状態をまとめることで計算量を削減する「対称性削減」や、長い循環動作への対応、より適切な分割方法の自動選択、SPINや記号的モデル検査ツールとのさらなる連携を進めていく予定です。
　こうした技術が発展すれば、多数の処理が同時に動く並行・分散ソフトウェアや大規模ハードウェアについて、設計上の不具合を開発の早い段階で発見しやすくなります。将来的には、安全で信頼できる情報システムの実現に貢献することが期待されます。

【用語説明】

【論文情報】

【研究資金】

　本研究は、日本学術振興会（JSPS）科学研究費助成事業（JP23K28060、JP23K19959、JP24K20757、JP24KK0185）の支援のもと行われたものです。

令和8年8月26日