多数の処理が同時に動く大規模情報システムでは、処理の組み合わせが増えるほど確認すべき動作が爆発的に増加する。その結果、計算機のメモリ不足により検証が未完了に終わったり、膨大な時間を要したりすることが大きな課題となっている。

そこで、考えられる動作を網羅的に調べる「モデル検査」に対し、大きな問題を細かく分割して解く「分割統治」の手法を取り入れ、複雑なソフトウェアやハードウェアが設計どおりに動作するかを、より少ないメモリで効率よく確認する新手法「DCA2MC」を、北陸先端科学技術大学院大学(JAIST)が開発。8月26日に発表した。

  • タブロー法による線形時相論理式の分解。複雑な条件が枝分かれしながら、より単純な条件へ分解される過程を示した図 (出所:JAIST Webサイト)

    タブロー法による線形時相論理式の分解。複雑な条件が枝分かれしながら、より単純な条件へ分解される過程を示した図 (出所:JAIST Webサイト)

同成果は、JAIST コンピューティング科学研究領域の緒方和博教授、同・髙木翼准教授、同・ド・ミン・カン講師らの研究チームによるもの。詳細は、米国計算機学会が刊行する、ソフトウェア工学全般を扱う専門論文誌「ACM Transactions on Software Engineering and Methodology」に掲載された。

大規模システムのモデル検査における課題

現在の情報システムでは、多数の処理が同時に行われ、互いに情報をやり取りしながら進行するため、実行順がわずかに変わるだけでも全体の動作が大きな影響を受ける。そのため、あらかじめ定めたパターンのみを試す従来型のテストでは、発生し得る全ての動作を検証して不具合を見つけることは困難だ。そこで利用されるのが「モデル検査」である。モデル検査は、システムが取り得る動作を網羅的に調べ、要求される性質を満たしているのかどうかを自動確認する技術だ。

しかし、システムが大きく複雑になるほど、確認すべき状態や動作の組み合わせは「状態空間爆発」を起こし、計算機のメモリ枯渇や検査時間の著しい長時間化を招く。これが、大規模システムにモデル検査を適用する上での大きな障壁となっている。

そうした中、研究チームは大きな問題を複数の小さな問題に分割して検査する「分割統治」のモデル検査への応用を進めてきた。しかし従来法では、検証する性質の種類ごとに異なる理論や支援ツールが必要という課題があった。そこで今回の研究では、論理式を一定の規則に従って分解する「タブロー法」を、検査すべき範囲の分割に応用することにしたという。

今回の研究成果

タブロー法は、複雑な論理式を、その意味を保ちながら一定規則に従ってより単純な論理式へ順番に分解する手法だ。モデル検査では、「ある状態が常に続く」「ある出来事が将来いつか起こる」といった、時間の流れに沿ったシステムの性質を表し、それが充足されるかが検証される。今回の研究では、そうした性質を記述する「線形時相論理」の式を、タブロー法を応用して分解する機能を形式仕様言語「Maude」上に実装し、新手法「DCA2MC」が開発された。

DCA2MCでは、検証範囲をまず複数層に分割する。この分割は、半自動的にも実行可能だ。層間の境界では、「次に何を確かめる必要があるか」という条件を次の層へ引き継ぎながら、検証が進められていく。こうして最終的に生成された小さな検査問題は、メモリ消費を抑えて検証できるため、大型計算機で巨大な問題全体を一度に扱う必要がなくなる。さらに、複数の計算機による並列処理も可能となり、検査時間の短縮も実現された。

  • 今回のアプローチによって分割された状態空間。システムが取り得る膨大な状態が複数の層に分けられ、それぞれが小さな検査問題として扱われる仕組みだ (出所:JAIST Webサイト)

    今回のアプローチによって分割された状態空間。システムが取り得る膨大な状態が複数の層に分けられ、それぞれが小さな検査問題として扱われる仕組みだ (出所:JAIST Webサイト)

しかし、大きな問題を小さく分割した場合、元の大きな問題と同一の正しい結論が得られるとは限らないという課題が生じる。そこで今回の研究では、分割後の全問題を検証した結果と、元の問題を直接検証した結果が一致するという数学的な証明がなされた。加えて、既存の並列モデル検査では、検査法自体を作り直す必要がある場合もあるが、DCA2MCは既存ツールを大きく変更せずに利用できるよう設計された。なお、DCA2MCは既存のモデル検査ツール「SPIN」との連携機能を備えている。

次に、DCA2MCの有効性を確かめるため、複数の処理が同じ資源を同時に利用しないよう調整する5種類の「相互排他プロトコル」(Qlock、Anderson、Ticket、MCS、TAS)を対象とする比較検証実験が行われた。実験では、「ある状態になった場合、その後いつか必ず別の状態になる」と「ある状態が将来のどこかで少なくとも一度は実現する」の2つの性質が主に調べられた。

その結果、「Qlock」では両性質について、「Anderson」と「Ticket」では前者の性質について、既存の代表的なモデル検査ツールである「SPIN」と「LTSmin」を用いて検証した結果、1テラバイトのメモリを消費しても完了できなかったとした。それに対し、DCA2MCはこれらの検証を完了できたという。さらに、分割された小規模な検査問題の並列処理によるモデル検査の高速化も確認された。

今回開発されたDCA2MCにより、膨大な検査問題を適切に小分けすることで、従来はメモリ容量や処理能力の制約から検証が難しかった大規模かつ複雑なシステムでも検証できる可能性が増大した。一方、類似な状態が多く現れる場合や、長い循環動作を含む場合には、分割効果が小さくなることがあるという。そのため、DCA2MCがあらゆる場面で既存の検査ツールよりも高速になるとは限らないとした。

研究チームは今後、類似状態をまとめることで計算量を削減する「対称性削減」や長い循環動作への対応、より適切な分割方法の自動選択、SPINや記号的モデル検査ツールとの連携深化を進めていく予定とする。こうした技術が発展すれば、多数の処理が同時に動く並行・分散ソフトウェアや大規模ハードウェアについて、設計上の不具合を開発の早い段階で発見しやすくなる。将来的には、安全で信頼できる情報システムの実現に貢献することが期待されるとしている。