| 研究課題/領域番号 |
22KJ0614
|
|---|
| 補助金の研究課題番号 |
21J21087 (2021-2022)
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 基金 (2023)
補助金 (2021-2022) |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
丁 曄澎 東京大学, 工学系研究科, 特別研究員(DC1)
|
|---|
| 研究期間 (年度) |
2023-03-08 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
2,200千円 (直接経費: 2,200千円)
2023年度: 700千円 (直接経費: 700千円)
2022年度: 700千円 (直接経費: 700千円)
2021年度: 800千円 (直接経費: 800千円)
|
|---|
| キーワード | ソフトウェア工学 / 情報セキュリティ / 分散コンピューティング / 形式手法 / プログラミング言語 / ブロックチェーン / 分散システム |
|---|
| 研究開始時の研究の概要 |
本研究は、信頼性の高い複雑なシステムの開発を促進するため、汎用アクション指向プログラミング（AOP）の理論基盤と実践方法論の構築を目的としている。AOPは、新しい視点から使いやすい形式手法を用いて、モデルの表現力と精度を向上し、低コストで実装の正当性を保証することで、正当性証明可能なシステムの開発をサポートするプログラミングパラダイムである。また、本研究では信頼性の高い分散システム、堅牢なプログラミングツール、および説明可能なAIモデルを開発するために、AOPを実用化し、現実的なフレームワークの構築を目標とする。
|
| 研究実績の概要 |
本研究では、複雑システムの正当性を数理的に保証するための理論基盤と実践方法論の構築を目的としている。今年度においては、形式的実装を実現に向けた遷移指向プログラミング(Transition-Oriented Programming)パラダイムの基本理論の構築し、特有の遷移指向プログラミング言語を実装した。そして、遷移指向プログラミングパラダイムと言語に基づき、様々な分野への応用研究を行った。これにより、信頼性の高い分散システムや堅牢なプログラミングツール、および説明可能なAIモデルを構築することが可能となった。
具体的には、グラフ遷移システム(Graph Transition System)理論を案出し、遷移システム理論と書き換えシステム理論を統一している。これで、システムの正当性を形式化し、時相型プロパティと関数型プロパティを同じ理論フレームワークに形式仕様記述、検証、実装することが可能となった。また、Seniという遷移指向プログラミング言語を実装し、グラフ遷移システム理論を実用化した。これにより、提案している遷移システム理論を分散コンピューティング、情報セキュリティ、ソフトウェア工学、暗号理論などの分野に応用した。例えば、検証したプロパティに基づき、正当性を保証する分権システム(Decentralized Systems)の形式的実装手法を提案した。また、自己主権型アイデンティティの枠組みの正当性を確保するための検証と実装するフレームワークを構築した。さらに、非中央集権型アプリ、特に分散型金融プロトコルの脆弱性を特定できる手法を実現した。研究成果は国際会議と論文誌で発表した。
|
