構造的動作意味定義に基づく実時間並行ソフトウェアの構築

• 研究課題/領域番号: 13680408
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 計算機科学
• 研究機関: 名古屋大学
• 研究代表者: 結縁 祥治 名古屋大学, 大学院・情報科学研究科, 助教授 (70230612)
• 研究期間 (年度): 2001 – 2003
• 研究課題ステータス: 完了 (2003年度)
• 配分額: 2,300千円 (直接経費: 2,300千円); 2003年度: 500千円 (直接経費: 500千円); 2002年度: 800千円 (直接経費: 800千円); 2001年度: 1,000千円 (直接経費: 1,000千円)
• キーワード: 実時間システム / プロセス代数 / 構造的動作意味定義 / 並行計算モデル / 構造的操作意味定義 / 実時間処理 / 合同性 / 優先度スケジューリング

研究概要

本研究で得られた主な結果は,構造的動作意味定義によって操作的意味論が与えられる時間付きプロセス言語に対する一般合同性定理である.この定理によってCCS, CSPなどの通信プロセス言語の時間拡張の形式的体系に対して一般的な代数的意味づけの枠組みが得られた.さらに,LOTOSにおいて時間決定性が保証されない原因を特定することができる.主結果は,Journal of Logic and Algebraic Programming誌に2004年中に掲載される予定である.
一般化定理は通信の結果生じる内部的な動作を抽象した弱等価性に対して得られる.構造的動作意味定義が本研究で得られた構文的条件を満たせば,合同性が一般的に保証される.さらに,時間に対しても時間経過として自然な性質を構想動作意味定義に対する構文条件として完全に近い形で特徴化できたと考えている.
一般化定理の実際的なプロセス言語への応用面に対して,本研究では目標としていたが,既存の処理系に基づいて解析を実施するにとどまった.この点については引き続き今後の課題である.その際には本研究で得られた結果が非常に一般的であるために,実用とされる領域への絞込みの技法としての型理論の研究,一部の機能を自然にモデル化するために名前通信を導入したπ計算の部分的な導入が必要であることが研究の結果得られた.

研究成果

• [文献書誌] I.Ulidowski, S.Yuen: "Process Languages with Discrete Realative Time based on the Ordered SOS Format and Rooted Eager Bisimulation"Journal of Logic and Algebraic Programming. (Elsevier, in Print). (2004)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 桑原寛明, 結縁祥治, 阿草清滋: "時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述"情報処理学会論文誌. (印刷中). (2004)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 深谷直彦, 結縁祥治, 阿草清滋: "実行可能なメモリモデルに基づくJava並行プログラムのモデル検査"ソフトウエア工学の基礎,FOSE2003レクチャーノート/ソフトウエア学(近代科学社). 227-238 (2003)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 水野敦, 真野健, 河辺義明, 桑原寛明, 結縁祥治, 阿草清滋: "π計算に基づくプログラミング言語NeipのためのGUI機能"情報処理学会プログラミング研究会,PRO. 48. 1-14 (2004)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] S.Yuen, K.Kato, D.Kato, S.Yamamoto, K.Agusa: "A Testing Framework for Web Applications based on the MVC model with Behavioral Description"Proceedings of International Conference on Information Technonology for Application 2004 (ICITA 2004). 11-1:1-6 (2004)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] I.Ulidowski, S.Yuen: "Process Languages with Discrete Relative Time based on the Ordered SOS Format and Rooted Eager Bisimulation"Journal of Algebraic and Logic Programmining (Elsevier). (in Print). (2004)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] H.Kuwabara, S.Yuen, K.Agusa: "A Formal Description of a Real-time Object-Oriented Language by the π-calculus with Time"Journal of Information Processing Society of Japan. (in Print). (2004)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] N.Fukaya, S.Yuen, K.Agusa: "Model Checking for Java Multithread Program based on the Executable Java Memory Model"Proceedings of Foundation of Software Engineering (F05E2003) (Kindai Kakagusha, (in Japanese)). 227-238 (2003)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] A.Mizuno, K.Mano, Y.Kawabe, H.Kuwabara, S.Yuen, K.Agusa: "Design and implementation of GUI for a pi-calculus-based programming language Nepi"Proceedings of Sig PRO 48,Information Processing Society of Japan. (2004)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] S.Yuen, K.Kato, D.Kato, S.Yamamoto, K.Agusa: "A Testing Framework for Web Applications based on the MVC model with Behavioral Description"Proceedings of International Conference on Internet Technology and Application ICITA2004. 11-4. 1-6 (2004)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] I.Ulidowski, S.Yuen: "Process Languages with Discrete Realative Time based on the Ordered SOS Format and Rooted Eager Bisimulation"Journal of Logic and Algebraic Programming(Elsevier). (採録決定). 1-76
• [文献書誌] 桑原寛明, 結縁祥治, 阿草清滋: "時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述"オブジェクト指向最前線2003,情報処理学会002003シンポジウム. 69-76 (2003)
• [文献書誌] 深谷直彦, 結縁祥治, 阿草清滋: "実行可能なメモリモデルに基づくJava並行プログラムのモデル検査"ソフトウエア工学の基礎,FOSE2003レクチャーノート/ソフトウェア学. 29. 227-238 (2003)
• [文献書誌] 水野敦, 真野健, 河辺義明, 桑原寛明, 結縁祥治, 阿草清滋: "π計算に基づくプログラミング言語NeipのためのGUI機能"情報処理学会プログラミング研究会. (発表予定). 1-14 (2004)
• [文献書誌] S.Yuen, K.Kato, D.Kato, S.Yamamoto, K.Agusa: "A Testing Framework for Web Applications based on the MVC model with Behavioral Description"International Conference on Information Technonology for Application 2004(ICITA 2004). 1-6 (2004)
• [文献書誌] K.Kato, S.Yuen, D.Kalo, K.Agusa: "Web Atulomata : A Behavioral Model of Web application based on the MVC model"第一回ディペンダブルソフトウェアワークショップ. 111-120 (2004)
• [文献書誌] Atsumi Noritoshi, Yuen Shoji, Yamamoto Shinichiro, Agusa Kiyoshi: "Library Evolution for Reliable Software"Proceedings of the workshop on Principles of software evolution. IWPSE02. 66-70 (2002)
• [文献書誌] I.Ulidowski, S.Yuen: "Timed Properties of Process Languages with Time"Proceesings of SCI2001, Vol XIV, IIIS. 344-349 (2001)
• [文献書誌] 大須賀恭輔, 結縁祥治, 阿草清滋: "実時間ステートチャートのためのプロセス言語"日本ソフトウェア科学会第18回大会講演論文集. 3A-2. 1-5 (2001)
• [文献書誌] 桑原寛明, 結縁祥治, 阿草清滋: "π計算による優先度継承プロトコルの形式的記述"情報処理学会プログラミング研究会 SIGPRO 2002-01. 11-1-11-10 (2002)
• [文献書誌] 大須賀恭輔, 結縁祥治, 阿草清滋: "実時間プロセス言語に基づく時間ステートチャートの動作シミュレーション"情報処理学会プログラミング研究会 SIGPRO 2002-01. 12-1-12-9 (2002)
• [文献書誌] 梶田将司, 結縁祥治: "NATによる準マルチホーム化技法"情報処理学会論文誌. 42巻12号. 2818-2826 (2001)