自己反映的ソフトウェアのための実行時検証とそのための仕様記述方式

• 研究課題/領域番号: 24500033
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 東京工業大学
• 研究代表者: 渡部 卓雄 東京工業大学, 情報理工学(系)研究科, 准教授 (20222408)
• 研究期間 (年度): 2012-04-01 – 2015-03-31
• 研究課題ステータス: 完了 (2014年度)
• 配分額: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円); 2014年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2013年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円); 2012年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
• キーワード: 自己反映計算 / 広域自己反映計算 / アクターモデル / 文脈指向プログラミング / 形式手法 / 実行時検証 / 並行文脈指向プログラミング / 並列文脈指向プログラミング / 実時間システム / 形式仕様 / 時相論理

研究成果の概要

アクターモデルを基盤とした広域自己反映計算モデルの形式化方式およびその検証手法の提案を行った．広域自己反映計算とは，並行計算系の総体的な構造・振舞を対象とする自己反映計算方式である．本研究では，個々のアクターのメタレベルを並列合成することでこの方式を実現し，並行文脈指向プログラミング等への応用を通してその有効性を示した．また，アクターモデルを含む言語や計算モデルについて，その性質記述および証明のモジュール化を可能にする条件を明らかにし，それにもとづく検証方式および証明の再利用方式を提案した．

研究成果

• [雑誌論文] Sandal: A Modeling Language Supporting Exhaustive Fault-Injection (2015)
  • 著者名/発表者名: Masaya Suzuki and Takuo Watanabe
  • 雑誌名: Theory and Practice of Computation 巻: 印刷中
  • 査読あり / 謝辞記載あり
• [雑誌論文] A Language Support for Exhaustive Fault-Injection in Message-Passing System Models (2014)
  • 著者名/発表者名: Masaya Suzuki and Takuo Watanabe
  • 雑誌名: Electronic Proceedings of Theoretical Computer Science 巻: 68 ページ: 45-58
  • DOI: 10.4204/eptcs.168.4
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] A Model-Checking Based Approach to Robustness Analysis of Procedures under Human-Made Faults (2014)
  • 著者名/発表者名: Naoyuki Nagatou and Takuo Watanabe
  • 雑誌名: Lecture Notes in Business Information Processing, 巻: 181 ページ: 117-131
  • DOI: 10.1007/978-3-319-08222-6_9
  • ISBN: 9783319082219, 9783319082226
  • 査読あり / 謝辞記載あり
• [雑誌論文] Compositional Construction of Group-Wide Meta-Level Architectures (2014)
  • 著者名/発表者名: Takuo Watanabe
  • 雑誌名: Theory and Practice of Computation 巻: 1 ページ: 95-107
  • DOI: 10.1142/9789814612883_0007
  • 査読あり / 謝辞記載あり
• [雑誌論文] Robustness Analysis on Human-made Faults in Procedural Manuals (2014)
  • 著者名/発表者名: Naoyuki Nagatou and Takuo Watanabe
  • 雑誌名: Theory and Practice of Computation 巻: 1 ページ: 79-94
  • DOI: 10.1142/9789814612883_0006
  • NAID: 110009769052
  • 査読あり / 謝辞記載あり
• [雑誌論文] Compositional Construction of Group-Wide Meta-Level Architectures (2014)
  • 著者名/発表者名: Takuo Watanabe
  • 雑誌名: Theory and Practice of Computation (World Scientific) 巻: －
  • 査読あり
• [雑誌論文] On Generating Soft Real-Time Programs for Non-Real-Time Environments (2013)
  • 著者名/発表者名: Ilankaikone Senthooran and Takuo Watanabe
  • 雑誌名: Theory and Practice of Computation (Springer PICT) 巻: 7 ページ: 1-12
  • DOI: 10.1007/978-4-431-54436-4_1
  • ISBN: 9784431544357, 9784431544364
  • 査読あり
• [雑誌論文] A Model-Based Approach to Constructing Safe Soft Real-Time Programs for Non-Real-Time Environments (2013)
  • 著者名/発表者名: Ilankaikone Senthooran and Takuo Watanabe
  • 雑誌名: Theory and Practice of Computation (Springer PICT) 巻: 7
  • 査読あり
• [雑誌論文] Modifiable Continuation in Object Calculus (2012)
  • 著者名/発表者名: Emiko Kuma, Shin-ya Nishizaki and Takuo Watanabe
  • 雑誌名: Theory and Practice of Computation (Springer PICT) 巻: 5 ページ: 160-173
  • DOI: 10.1007/978-4-431-54106-6_13
  • ISBN: 9784431541059, 9784431541066
  • 査読あり
• [雑誌論文] Abstraction of Operations of Aspect-Oriented Languages (2012)
  • 著者名/発表者名: Sosuke Moriguchi and Takuo Watanabe
  • 雑誌名: Theory and Practice of Computation (Springer PICT) 巻: 5 ページ: 187-201
  • DOI: 10.1007/978-4-431-54106-6_15
  • NAID: 110007970928
  • ISBN: 9784431541059, 9784431541066
  • 査読あり
• [雑誌論文] 定理証明支援系Coqへの対話的修正機構の導入 (2012)
  • 著者名/発表者名: 森口草介, 渡部卓雄
  • 雑誌名: 情報処理学会論文誌 プログラミング(PRO) 巻: 5(4) ページ: 27-38
  • NAID: 40019468752
  • 査読あり
• [学会発表] 小規模組み込みシステムにおけるFRPの応用に向けて (2015)
  • 著者名/発表者名: 澤田賢祐, 鈴木康平, 渡部卓雄
  • 学会等名: 電子情報通信学会ソフトウェアサイエンス研究会(SIGSS)
  • 発表場所: 熊本大学・黒髪キャンパス
  • 年月日: 2015-05-11 – 2015-05-12
• [学会発表] アクターモデルに基づく並行文脈指向プログラミング機構の実装と評価 (2014)
  • 著者名/発表者名: 竹野創平, 渡部卓雄
  • 学会等名: 日本ソフトウェア科学会第31回大会
  • 発表場所: 名古屋大学・東山キャンパス
  • 年月日: 2014-09-07 – 2014-09-10
• [学会発表] Aπ計算のCoqによる形式化 (2014)
  • 著者名/発表者名: 安武祥平, 渡部卓雄
  • 学会等名: 日本ソフトウェア科学会第31回大会
  • 発表場所: 名古屋大学・東山キャンパス
  • 年月日: 2014-09-07 – 2014-09-10
• [学会発表] A Reflective Approach to Actor-Based Concurrent Context-Oriented Systems (2014)
  • 著者名/発表者名: Takuo Watanabe and Souhei Takeno
  • 学会等名: 6th International Workshop on Context-Oriented Programming (COP 2014) （査読あり）
  • 発表場所: Uppsala University
  • 年月日: 2014-07-29
• [学会発表] A Model-Checking Based Approach to Robustness Analysis of Procedures under Human-Made Faults (2014)
  • 著者名/発表者名: Naoyuki Nagatou, Takuo Watanabe
  • 学会等名: 2nd Asia Pacific Conference on Business Process Management (APBPM 2014, Springer LNBIP, Vol. 181, pp. 121-135) (査読有)
  • 発表場所: Queensland University of Technology, Brisbane
• [学会発表] ヒューマンエラーに対する手順書の耐性検査 (2013)
  • 著者名/発表者名: 永藤直行, 渡部卓雄
  • 学会等名: 電子情報通信学会知能ソフトウェア工学研究会 (信学技報 Vol. 113, No. 71, pp. 61-66)
  • 発表場所: 慶應義塾大学・日吉キャンパス
• [学会発表] 人為的欠陥の意味と耐性解析 (2013)
  • 著者名/発表者名: 永藤直行, 渡部卓雄
  • 学会等名: 日本ソフトウェア科学会第30回大会
  • 発表場所: 東京大学・本郷キャンパス
• [学会発表] Robustness Analysis on Human-made Faults in Procedural Manuals (2013)
  • 著者名/発表者名: Naoyuki Nagatou, Takuo Watanabe
  • 学会等名: Workshop on Computation: Theory and Practice (WCTP 2013, pp. 69-81) (査読有)
  • 発表場所: University of the Philippines, Diliman
• [学会発表] A Compositional Reflective Architecture for Actor-Based Systems (2013)
  • 著者名/発表者名: Takuo Watanabe
  • 学会等名: Workshop on Computation: Theory and Practice (WCTP 2013, pp. 1-12) (査読有)
  • 発表場所: University of the Philippines, Diliman
• [学会発表] Towards a Compositional Reflective Architecture for Actor-Based Systems (2013)
  • 著者名/発表者名: Takuo Watanabe
  • 学会等名: 3rd ACM International Workshop on Programming based on Actors, Agents, and Decentralized Control (AGERE!SPLASH 2013, pp. 19-24) (査読有) DOI: /10.1145/2541329.2541341
  • 発表場所: Hyatt Regency, Indianapolis
• [学会発表] 検証付きプログラムに対する対話的修正の合成 (2013)
  • 著者名/発表者名: 森口草介, 渡部卓雄
  • 学会等名: 日本ソフトウェア科学会FOSE2013 (レクチャーノート/ソフトウェア学, Vol. 39, pp. 131-136) (査読有)
  • 発表場所: 加賀市山代温泉
• [学会発表] 実時間システム向け文脈指向言語ProcneJ (2013)
  • 著者名/発表者名: 安原由貴, 森口草介, 渡部卓雄
  • 学会等名: 情報処理学会プログラミング研究会
  • 発表場所: 国立情報学研究所(東京都千代田区)
• [学会発表] 実時間システム向けの文脈指向DSL (2013)
  • 著者名/発表者名: 中村遼太郎, 渡部卓雄
  • 学会等名: 情報処理学会ソフトウェア工学研究会
  • 発表場所: 化学会館(東京都千代田区)
• [学会発表] An Interactive Extension Mechanism for Reusing Verified Programs (2013)
  • 著者名/発表者名: Sosuke Moriguchi and Takuo Watanabe
  • 学会等名: 28th ACM Symposium on Applied Computing (査読有)
  • 発表場所: Institute of Engineering of the Polytechnic Institute of Coimbra (Coimbra, Portugal)
• [学会発表] ヒューマンエラーに対する手順書の耐性検査 (2013)
  • 著者名/発表者名: 永藤直行, 渡部卓雄
  • 学会等名: 電子情報通信学会知能ソフトウェア工学研究会
  • 発表場所: 慶應義塾大学(神奈川県横浜市)
• [学会発表] Objective-Cによる文脈指向プログラミングの実現手法 (2012)
  • 著者名/発表者名: 鈴木将哉, 渡部卓雄
  • 学会等名: 電子情報通信学会ソフトウェアサイエンス研究会
  • 発表場所: はこだて未来大学(北海道函館市)
• [学会発表] A Model-Based Approach to Constructing Safe Soft Real-Time Programs for Non-Real-Time Environments (2012)
  • 著者名/発表者名: Ilankaikone Senthooran and Takuo Watanabe
  • 学会等名: 13th ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing (SNPD 2012) (査読有)
  • 発表場所: キャンパスプラザ京都(京都市)
• [学会発表] 組込みシステムのための文脈指向仕様記述に向けて (2012)
  • 著者名/発表者名: 安原由貴, 森口草介, 渡部卓雄
  • 学会等名: 日本ソフトウェア科学会第29回大会
  • 発表場所: 法政大学(東京都小金井市)
• [学会発表] On Generating Soft Real-Time Programs for Non-Real-Time Environments (2012)
  • 著者名/発表者名: Ilankaikone Senthooran and Takuo Watanabe
  • 学会等名: Workshop on Computation: Theory and Practice (WCTP 2012) (査読有)
  • 発表場所: De La Salle University (Manila)
• [備考] Sandal
  • URL: https://github.com/draftcode/sandal