2021 Fiscal Year Annual Research Report
Formal Methods in General-Purpose Action-Oriented Programming
| Project/Area Number |
21J21087
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
丁 曄澎 東京大学, 工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2021-04-28 – 2024-03-31
|
| Keywords | ソフトウェア工学 / 形式手法 / 分散システム / プログラミング言語 / ブロックチェーン / 情報セキュリティ |
|---|
| Outline of Annual Research Achievements |
本研究では、形式手法によって堅牢なシステムを実現する汎用アクション指向プログラミングパラダイムを提案する。具体的には、まず、使いやすい形式仕様記述手法を新たなモデリング言語に実装する。そして、形式的検証とプログラムの生成を自動で行うアルゴリズムをもとに、信頼できる分散システムや堅牢なプログラミングツール、および説明可能なAIモデルを構築する。
本年度は、遷移システム理論と自動プログラミング手法に基づく形式主義駆動の開発手法とその実用化をする研究を行なってきた。開発工程の視点から、形式手法を中心として設計、検証、実装、統合をアジャイル開発に統一する理論とフレームワークを提案した。定式化した遷移システムのバリアントを用いて、システムの構造と挙動を抽象化することで、形式的検証できるプログラムと実行できるテムプレートが自動的に生成できる手法を試みた。特に、分散システムの開発に応用し、コンセンサスメカニズムなどの実装過程で提案手法を実証した。研究結果は国際会議と論文誌で発表した。
さらに、本研究では、汎用アクション指向プログラミングの有効性と適用性の実証のため、分散システムのセキュリティとプライバシーに関する研究も行なった。公開ブロックチェーン上でのデータ共有や自己主権型アイデンティティの枠組みなどの中で、アクション指向プログラミングを用いてプロトコルの設計と検証を行い、安全性について分析した。上記の研究結果について国際会議と国内会議で発表した。
また、汎用アクション指向プログラミングを実用化するため、形式手法の改善を行なっている。特に、正当性証明可能なシステムの生成メカニズムの最適化を模索している。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
当該年度では、汎用アクション指向プログラミングの理論構築を中心に研究を行い、実用化の可能性を探った。主著での国際会議採択が３件，国内会議発表が1件，国際誌採択が1件となったが、理論構築を進める上で困難が生じた。特に、従来の形式手法の有用性とユーザビリティのバランスと、新たな手法が学界と業界に認められるための工夫を凝らすことが予想以上に難しいと実感した。当初の研究計画より、ワークロードが高くなった。新たなプログラミングパラダイムの有効性を示すため、多様な分野で実証する必要があると考えている。
|
| Strategy for Future Research Activity |
今後は、汎用アクション指向プログラミングの理論構築と実用化のバランスに注力する予定である。提案手法の実用可能性を広げるため、形式的検証と実行メカニズムを統一するプログラミング言語を実装し、主にブロックチェーン、モデル検査、ニューラルネットワークの三つの分野に応用し、実証を行う。また、実用化を推進する過程に、新たに発見した問題を抽象化し、理論基盤を調整していく。このようにして、堅牢性が高まるよう研究を進めていく予定である。研究結果は国際会議、または論文誌で発表することを目指している。
|
