Formal Methods in General-Purpose Action-Oriented Programming
| Project/Area Number |
22KJ0614
|
|---|
| Project/Area Number (Other) |
21J21087 (2021-2022)
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Multi-year Fund (2023)
Single-year Grants (2021-2022) |
|---|
| Section | 国内 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
丁 曄澎 東京大学, 工学系研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2023-03-08 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2023: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2022: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2021: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | ソフトウェア工学 / 情報セキュリティ / 分散コンピューティング / 形式手法 / プログラミング言語 / ブロックチェーン / 分散システム |
|---|
| Outline of Research at the Start |
本研究は、信頼性の高い複雑なシステムの開発を促進するため、汎用アクション指向プログラミング（AOP）の理論基盤と実践方法論の構築を目的としている。AOPは、新しい視点から使いやすい形式手法を用いて、モデルの表現力と精度を向上し、低コストで実装の正当性を保証することで、正当性証明可能なシステムの開発をサポートするプログラミングパラダイムである。また、本研究では信頼性の高い分散システム、堅牢なプログラミングツール、および説明可能なAIモデルを開発するために、AOPを実用化し、現実的なフレームワークの構築を目標とする。
|
| Outline of Annual Research Achievements |
本研究では、複雑システムの正当性を数理的に保証するための理論基盤と実践方法論の構築を目的としている。今年度においては、形式的実装を実現に向けた遷移指向プログラミング(Transition-Oriented Programming)パラダイムの基本理論の構築し、特有の遷移指向プログラミング言語を実装した。そして、遷移指向プログラミングパラダイムと言語に基づき、様々な分野への応用研究を行った。これにより、信頼性の高い分散システムや堅牢なプログラミングツール、および説明可能なAIモデルを構築することが可能となった。
具体的には、グラフ遷移システム(Graph Transition System)理論を案出し、遷移システム理論と書き換えシステム理論を統一している。これで、システムの正当性を形式化し、時相型プロパティと関数型プロパティを同じ理論フレームワークに形式仕様記述、検証、実装することが可能となった。また、Seniという遷移指向プログラミング言語を実装し、グラフ遷移システム理論を実用化した。これにより、提案している遷移システム理論を分散コンピューティング、情報セキュリティ、ソフトウェア工学、暗号理論などの分野に応用した。例えば、検証したプロパティに基づき、正当性を保証する分権システム(Decentralized Systems)の形式的実装手法を提案した。また、自己主権型アイデンティティの枠組みの正当性を確保するための検証と実装するフレームワークを構築した。さらに、非中央集権型アプリ、特に分散型金融プロトコルの脆弱性を特定できる手法を実現した。研究成果は国際会議と論文誌で発表した。
|
Report
(3 results)
Research Products
(21 results)
