研究課題
証明スコア法により問題仕様(問題領域や応用領域における組織、規則、活動、処理の仕様やモデル)の検証を可能とする革新的仕様検証技術の開発を目指して研究を行い、以下の成果を得た。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)に基づく形式仕様開発方法論の有効性を確認した。
すべて 2011 その他
すべて 雑誌論文 (7件) (うち査読あり 7件) 学会発表 (1件) 備考 (1件)
IEICE Transactions
巻: 94-A(9) ページ: 1877-1880
IEICE TRANSACTIONS on Information and Systems
巻: E94-D(5) ページ: 976-988
Proc.of 2011 World Congress on Computer Science and Information Engineering (CSIE 2011), Lecture Notes in Electrical Engineering, Springer
巻: (印刷中)
Proc.of The Fifth International Conference on Secure Software Integration and Reliability Improvement Companion (IEEE SSIRI-C 2011)
ページ: 187-193
18th IEEE International Conference and Workshops on Engineering of Computer-Based Systems (ECBS 2011)
ページ: 130-139
IEEE International Conference on Web Services (ICWS 2011)
ページ: 722-723
Proc.of 18^<th> Asia-Pacific Software Engineering Conference (APSEC 2011)
ページ: 274-281
http://www.ldl.jaist.ac.jp/cafeobj/
