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

2003 Fiscal Year Annual Research Report

• Project/Area Number: 13680408
• Research Institution: Nagoya University
• Principal Investigator: 結縁 祥治 名古屋大学, 大学院・情報科学研究科, 助教授 (70230612)
• Keywords: 実時間システム / プロセス代数 / 構造的動作意味定義

Research Abstract

本年度は,本研究で得られた主結果である時間プロセス言語に対する合同性定理と時間的性質につ いて,海外協力者であるUlidowski博士とともに結果をまとめ学術論文誌に投稿した.Journal of Logic and Algebraic Programming誌より採録との結果を受け取っている.
昨年度に引き続き,ソフトウェアシステムに対する応用についての検討を行った.
1. π計算に対して本結果で得られた拡張を行い,単純な並行オブジェクト指向計算言語の振舞いを定式化した.並行オブジェクト言語の振舞いがいくつかの時間的性質を満たすことを示した.ここでは,弱等価性に基づいて並行オブジェクトの意味を定義した.
2.π計算を直接的に実行するプログラミング言語Nepiにおいて,グラフィックユーザインタフェース機構の拡張を行った.プログラミング言語Nepiには時間の概念が含まれており,意味論の検討には本研究の手法が応用できる.
3.Webシステムのオートマトンに基づくモデル化を行った.現時点では,形式システムへの定式化がまだ十分行われていない.しかし,パフォーマンスを考慮したWebシステムの定式化に対して本研究の結果が応用できることが期待できる.
本研究における検討の結果,ソフトウェアシステムに対する応用においては,本研究で得られたモデルをそのまま応用することは不十分であることが判明しているので,型理論に基づくソフトウェアシステムへの制約,本研究のπ計算などの名前渡し体系への拡張を検討することは今後の課題である.

Research Products

• [Publications] 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
• [Publications] 桑原寛明, 結縁祥治, 阿草清滋: "時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述"オブジェクト指向最前線2003,情報処理学会002003シンポジウム. 69-76 (2003)
• [Publications] 深谷直彦, 結縁祥治, 阿草清滋: "実行可能なメモリモデルに基づくJava並行プログラムのモデル検査"ソフトウエア工学の基礎,FOSE2003レクチャーノート/ソフトウェア学. 29. 227-238 (2003)
• [Publications] 水野敦, 真野健, 河辺義明, 桑原寛明, 結縁祥治, 阿草清滋: "π計算に基づくプログラミング言語NeipのためのGUI機能"情報処理学会プログラミング研究会. (発表予定). 1-14 (2004)
• [Publications] 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)
• [Publications] K.Kato, S.Yuen, D.Kalo, K.Agusa: "Web Atulomata : A Behavioral Model of Web application based on the MVC model"第一回ディペンダブルソフトウェアワークショップ. 111-120 (2004)