モデル検査ツールUPPAALを用いたGALSシステムの形式的検証

摘要

GALS(Globally Asynchronous Locally Synchronous)システムの設計では，設計したシステムが意図した通りに動作することを検証する必要がある．GALSシステムは非同期通信を行うため，検証を行うには連続時間性を考慮してモデル化しなければならない．しかし，従来の検証手法ではこの点が十分に考慮されていなかった．本研究では，連続時間に基づく検証ツールUPPAALを用いて，GALSシステムの設計を形式的に検証する手法を提案している．STPN (Stochastic Timed Petri Nets)でモデル化されたGALSシステムを，UPPAALで扱う拡張時間オートマトンに変換する手法を提案し，ツールとして実装している．適用例として，STPNで記述されたGALSシステムに提案法を適用して検証を行い，手法の有効性を確認している．