Modeling Techniques for real-time concurrent software based on the Structural Operationl Semantics

基于结构操作语义的实时并发软件建模技术

• 批准号: 13680408
• 负责人: YUEN Shoji
• 金额: $ 1.47万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13680408/
• 关键词: Real time system; Process Calculi; Structural Operational Semantics; 並行計算モデル; 構造的操作意味定義; 実時間処理; 合同性; 優先度スケジューリング

The main result of this research is the uniform congruence theorem for timed process languages, which is to be published as a full paper in Journal of Algebraic and Logic Programming in 2004. This theorem characterizes not only the algebraic congruence for timed process languages but also the interesting timed properties that is essential for discrete time modeling by the syntactic format of Structural Operational Semantics. Our characterization explains the weak semantics of most of all the existing timed process calculi, such as timed CCS and timed CSP. It solves the difficulties of timed process languages and extends the defininability of the timed process languages in an abstract way. This fact is useful to model the real-time concurrent software using the process calculi techniques.For the practical applications to the software modeling, we found out that our result is still too general. We continue to investigate (1)the type theory to focus on the more interesting class of timed process calculi and (2)incorporation of name-passing of pi-calculus to model the software in a simple manner.

这项研究的主要成果是时间过程语言的一致同余定理，这是作为一个完整的论文发表在代数和逻辑编程杂志在2004年。该定理不仅描述了时间过程语言的代数全等性，还描述了有趣的时间性质，这些性质对于通过结构操作语义的语法格式进行离散时间建模至关重要。我们的表征解释了大多数现有的定时进程演算，如定时CCS和定时CSP的弱语义。它解决了时间过程语言的困难，并以抽象的方式扩展了时间过程语言的可定义性。这一事实对于利用进程演算技术对实时并发软件进行建模是有用的。我们继续研究（1）类型理论，专注于更有趣的时间进程演算类和（2）合并pi演算的名称传递，以简单的方式对软件进行建模。

项目成果

水野敦, 真野健, 河辺義明, 桑原寛明, 結縁祥治, 阿草清滋: "π計算に基づくプログラミング言語NeipのためのGUI機能"情報処理学会プログラミング研究会,PRO. 48. 1-14 (2004)

Atsushi Mizuno、Ken Mano、Yoshiaki Kawabe、Hiroaki Kuwabara、Shoji Yuen、Kiyoji Asakusa：“基于 π 演算的编程语言 Neip 的 GUI 函数”日本信息处理协会编程研究组，PRO 48. 1-14 (2004)。

桑原寛明, 結縁祥治, 阿草清滋: "π計算による優先度継承プロトコルの形式的記述"情報処理学会プログラミング研究会 SIGPRO 2002-01. 11-1-11-10 (2002)

Hiroaki Kuwabara、Shoji Yuen 和 Kiyoji Asakusa：“使用 π 计算对优先级继承协议的正式描述”日本信息处理协会编程研究小组 SIGPRO 2002-01 (2002)。

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

S.Yuen、K.Kato、D.Kato、S.Yamamoto、K.Agusa：“基于具有行为描述的 MVC 模型的 Web 应用程序测试框架”2004 年国际应用信息技术会议论文集 (ICITA 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)

K.Kato、S.Yuen、D.Kalo、K.Agusa：“Web Atulomata：基于 MVC 模型的 Web 应用程序行为模型”第 1 届 Dependable Software Workshop（2004 年）。

I.Ulidowski, S.Yuen: "Timed Properties of Process Languages with Time"Proceesings of SCI2001, Vol XIV, IIIS. 344-349 (2001)

I.Ulidowski、S.Yuen：“过程语言的时间属性与时间”SCI2001 论文集，第 XIV 卷，IIIS。