証明スコア法に基づく革新的仕様検証技術の研究

点击翻译按钮获取中文摘要

証明スコア法により問題仕様(問題領域や応用領域における組織、規則、活動、処理の仕様やモデル)の検証を可能とする革新的仕様検証技術の開発を目指して研究を行い、以下の成果を得た。1適切な抽象度の実現法について、提案している観測遷移シヌテム(OTS:Observational Transition System)がデータ型とプロセス型を適切に定義することで、適切な抽象度を実現する一般的なスキーマと成り得ることを、実用規模の事例開発を通じて確認した。2推論型×探索型検証法の実現法について、(1)帰納法に基づく反例発見法(IGF:Induction Guided Falsification)と(2)推論に基づく抽象化と探索に基づく反例発見を組み合わせる方法、の2つの方法が有効であることを例題に基づき確認した。3電子商取引プロトコル事例については、上記の「推論型×探索型検証法」を実例に基づき確認することに焦点を当てて研究を行った。具体的にはiKP(Internet Keyed Payment Protocols)を取り上げ、帰納法に基づく反例発見法(IGF)の有効性を確認した。この事例開発では、CafeOBJ言語システムで形式仕様を開発し、Maude言語システムの高効率の探索機能を利用する方法論についても研究を行い、そのための方法論と支援ツールも開発した。4車載OS標準事例については、AUTOSARが公開し世界的に認知度が高いOSEK/VDX仕様(portal.osek-vdx.org/files/pdf/specs/os223.pdf)に対して、CafeOBJ言語で記述された形式仕様を開発した。この仕様開発において、観測遷移システム(OTS)に基づく形式仕様開発方法論の有効性を確認した。