A Fundamental Research for Formal Models and Verification Techniques of Open Software

开放软件形式化模型与验证技术的基础研究

• 批准号: 08458066
• 负责人: INAGAKI Yasuyoshi
• 金额: $ 4.99万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 1997
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08458066/
• 关键词: Concurrency; Communicating Processes; Formal Semantics; Programming Environment; Debuggin Procedure; ネットワーク; 並行システム; 項書換え系; 検証; 実時間システム; メタ計算モデル

We have investigated the appropriate formal framework for "open software" that behaves reactively on communications with the environment. Based on the communicating process model, we mainly focused on establishing the formal semantics and the verification techniques of open software. The results we have achieved are listed as follows :(1) We proposed a timed extension to the communicating process model and derived an effecient alternative characterization for verification.(2) We also proposed a probabilistic extension to the communication process model and derived effecient alternative characterizations for verification.(3) We presented a general framework for "Structural Operational Semantics" specification to have the congruence and the well-definedness of "time".(4) We investigated a logical characterization of open software by the multi-autoepistemic logic.(5) We build a prototype programming environment for an efficient debugging based on the diagnostic information generation.(6) We proposed a intermidiate description that can be abstracted as a LOTOS specification and also can be expanded as a C-program at the same time.

我们研究了“开放软件”的适当正式框架，该框架在与环境的通信中做出反应。基于通信过程模型，我们主要致力于建立开放软件的形式语义和验证技术。我们取得的成果如下：（1）我们提出了通信过程模型的定时扩展，并导出了有效的替代表征以进行验证。（2）我们还提出了通信过程模型的概率扩展，并导出了有效的替代方案(3)我们提出了“结构操作语义”规范的通用框架，以具有“时间”的一致性和明确定义性。(4)我们研究了“时间”的逻辑表征(5)我们构建了一个基于诊断信息生成的高效调试原型编程环境。(6)我们提出了一种可以抽象为LOTOS规范并且可以扩展的中间描述同时作为 C 程序。

项目成果

K.Kawaguchi: "TERSE : A Visual Environment for Supporting Analysis,Verification and Transformation of Term Rewriting Systems" Proceedings of AMAST'96 (LNCS 1101). 571-574 (1996)

K.Kawaguchi：“TERSE：支持术语重写系统分析、验证和转换的可视化环境”AMAST96 论文集 (LNCS 1101)。

河口信夫: "項書換え系における書換え系列の視覚化の拡張-中間実行とフィルター" 電気関係学会東海支部連合大会講演論文集. 659-659 (1996)

Nobuo Kawaguchi：“术语重写系统中重写序列的可视化扩展 - 中间执行和过滤器”日本电气工程师东海分会会议记录 659-659 (1996)。

K.Toyama, Y.Inagaki, A.Fukumura: "Representation of Persistence and Causality Based on Multi-Autoepistemic Logic" Journal of JSAI. Vol.12 (in Japanese). 466-474 (1997)

K.Toyama、Y.Inagaki、A.Fukumura：“基于多重自我认知逻辑的持久性和因果关系的表示”，JSAI 期刊。

鈴木晃: "SCCS動作式に対するunfold変換によるLTSモデルの効率的構成法" 電子情報通信学会技術報告. COMP96-47. 93-100 (1997)

Akira Suzuki：“使用 SCCS 运动方程展开变换的 LTS 模型的高效构建方法”IEICE 技术报告 93-100 (1997)。

外山 勝彦、稲垣 康善、福村 晃夫: "多エージェント系自己認識論理に基づく状態継続と因果関係の表現" 人工知能学会論文誌. Vol.12. 466-474 (1997)

Katsuhiko Toyama、Yasuyoshi Inagaki、Akio Fukumura：“基于多智能体自我识别逻辑的状态延续和因果关系的表示”人工智能学会期刊 12. 466-474 (1997)。