Research on the method for reactive system construction by using a modal structural description language

模态结构描述语言构建反应式系统方法研究

• 批准号: 03680027
• 负责人: YONEZAKI Naoki
• 金额: $ 1.34万
• 依托单位: Japan Advanced Institute of Science and Technology,Hokuriku
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1991
• 资助国家: 日本
• 起止时间: 1991 至 1992
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-03680027/
• 关键词: Specification; Theorem proving; Object Base; Executable specification; Unification; Realizability; 様相論理; 定理自動証明; 定理証明; オブジェクトベ-ス; 実行可能仕様; 統一化

Application of non-standard logic to software development is our main concern.(1) Multi-modal logic for specification of reactive objects: We have developed multi modal logic (MML) which has temporal modality and object modality as well. Formalization of object modalities reflecting has a and is a relations was one of our main concern. For the temporal aspects, we developed a new decidable temporal logic which is more expressive than the usual temporal logics in the sense that we can describe the relation on the number of event occurrences so that we can define more sophisticated fairness notion.(2)Automated reasoning in non-standard logic: Theorem proving methods for non-standard logic was studied. For the various kind of modal logic, we developed a general theorem prover which utilizes modal unification. We discovered some unification schema which drastically deduce the number of steps of proofs. This schema incorporate cyclic unification so called self-unification. We also developed a resolution style theorem prover for linear logic as a basis of new computation paradigm.(3) Verification and synthesis of programs: A transformation system from specifications to reactive system programs was developed based on the tableau based model generation system. We introduced several realizability concepts and their decision procedures with which we can design a helpful method for getting proper specifications from those with failure or incompleteness.(4) Model for work process specification: Planning, scheduling, enacting and evaluating human activity is framework of our daily working process. To describe this, we are developing a model for this kind of work process specifications. The first class objects of the model are Tasks, Agents and Products (TAP). This model has several dimensions i.e. meta-object, abstract-instance, structural hierarchy and temporal dimensions.

在软件开发中应用非标准逻辑是我们主要关心的问题。(1)反应性对象规范的多模态逻辑：我们开发了多模态逻辑（MML），它同时具有时间模态和对象模态。对象模态的形式化反映有和是一种关系是我们主要关注的问题之一。在时间方面，我们开发了一种新的可决时间逻辑，它比通常的时间逻辑更具表现力，因为我们可以描述事件发生次数的关系，从而可以定义更复杂的公平性概念。(2)非标准逻辑中的自动推理：研究了非标准逻辑的定理证明方法。对于各种模态逻辑，我们发展了一个利用模态统一的一般定理证明。我们发现了一些统一的模式，大大减少了证明的步骤数。这种模式包含循环统一，也就是所谓的自统一。我们还开发了一个线性逻辑的解析式定理证明，作为新的计算范式的基础。(3)程序的验证与综合：在基于表格的模型生成系统的基础上，开发了从规范到反应系统程序的转换系统。本文介绍了几个可实现性概念及其决策过程，利用这些概念和决策过程，我们可以设计一种有用的方法，从失败或不完整的产品中获得适当的规格说明。(4)工作流程规范模型：计划、调度、实施和评估人类活动是我们日常工作流程的框架。为了描述这一点，我们正在为这类工作过程规范开发一个模型。模型的第一个类对象是任务、代理和产品（TAP）。该模型具有元对象、抽象实例、结构层次和时间维度。

项目成果

Takehiro Tokuda: "Research Topics of Interactive Document Systems" Proc.of 3rd Symp.on Software Engineering and Computer Graphics,Univ.of Washington. 1-4 (1991)

Takehiro Tokuda：“交互式文档系统的研究主题”Proc.of 3rd Symp.on Software Engineering and Computer Graphics，华盛顿大学。

Naoki Yonezaki,Takeshi Hayama: "Advances in Information Modeling and Knowledge Bases" ISO press, 16 ヨC (1993)

Naoki Yonezaki、Takeshi Hayama：“信息模型和知识库的进展”ISO press，16 YoC (1993)

宮川 晋: "MSLによる仕様記述のコンパイル方式" 日本ソフトウェア科学会第8回大会論文集. 329-332 (1991)

Susumu Miyakawa：“使用 MSL 的规范描述的编译方法”日本软件学会第八届年会论文集 329-332（1991）。

Noriaki Yoshiura,Naoki Yonezaki: "More expressive Temporal Logic for Specifications" The fifth International Conference on Software Engeering and Knowledge Engeering. (1993)

Noriaki Yoshiura、Naoki Yonezaki：“规范的更具表现力的时间逻辑”第五届软件工程和知识工程国际会议。

Ryousei Mori,Naoki Yonezaki: "Several realizability concepts in reactive objects" Proceeding of 2nd European-Japanese Seminar on Information modelling and knowledge Bases. (1993)

Ryousei Mori、Naoki Yonezaki：“反应对象中的几个可实现性概念”第二届欧洲-日本信息建模和知识库研讨会论文集。