2008 Fiscal Year Annual Research Report
テストに基づく補題発見を用いた安全性自動検証器の開発
| Project/Area Number |
20800082
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
中野 昌弘 National Institute of Advanced Industrial Science and Technology, システム検証研究センター, 産総研特別研究員 (90470046)
|
|---|
| Keywords | 仕様記述・仕様検証 / 数理論理学 / 並列分散処理 / アルゴリズム工学 |
|---|
| Research Abstract |
まず不変性だけでなく、その一般化である安全性の検証を行うために、安全性をBuchiオートマトンで定式化した。安全性を帰納法により証明するため、証明義務の定式化を行い、不動点帰納法で実装するための手続きを定義した。また、不変性に対する不動点帰納法で行っていた補題発見法が、同様に適用できることを確認した。と同時に、残念ながら安全性に対する補題発見は、多くの場合、組み合わせ爆発により計算量が増大しやすいことも明らかになった。同様の問題は、不変性検証においても起こりうるものであり、実際、NSLPKプロトコルを不変性検証器で検証したときに、認証性と秘匿性を同時に与えたときは、証明に成功したものの、認証性のみでは同様の原因で証明に失敗した。しかしながら定式化した結果から、不変性に対する証明法から自然に安全性に対する証明法へ拡張できることも確認できたため、まず不変性に対して、SMTによる検証能力の向上と、並列化による検証の効率化を図る方針へと変更した。
変更した方針に基づいて実装を開始した。多くのSMTの実装では、充足可能性を検査するのに必要最低限のインタフェースしか提供しておらず、最弱事前条件計算に利用できなかった。幸いソースコードが公開されたSMTの実装としてCVC3を得ることができたため、CVC3を利用することにした。SMTを用いて不動点帰納法を実現することは容易であると期待したが、充足可能性を検査するための最適化と、最弱事前条件を計算するための最適化は大きく異なり、予想以上にSMTの振る舞いを変更する必要があることが明らかになった。CVC3上で簡易的な不動点帰納法を実装したものの、この最適化の違いにより最弱事前条件を求めることができなかった。この最適化を抑制するためには、CVC3をより詳細に理解する必要があり、現状ではこの調査を行っている。
またBuchiオートマトンで安全性を定式化する過程で、安全性・余安全性に対する全反例を、有限オートマトンに対する手続きにより、効率的に求められることを明らかにし、システム検証の科学技術シンポジウムにて発表した。
|
