Research on construction of embedded software using formal object-oriented methods

采用形式化面向对象方法构建嵌入式软件的研究

• 批准号: 12480071
• 负责人: KATAYAMA Takuya
• 金额: $ 4.8万
• 依托单位: JAPAN ADVANCED INSTITUTE OF SCIENCE AND TECHNOLOGY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2000
• 资助国家: 日本
• 起止时间: 2000 至 2002
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-12480071/
• 关键词: object-oriented method; embedded system; analysis model; formal method; theorem proving system; concurrent regular expression; thread; concurrent object; 組み込みシステム; 定理証明; 形式的オブジェクト指向方法論; オブジェクト; 実時間OS

We studied on the application of formal object-oriented methods to the construction of embedded system. First, we studied on the environment to construct formal object-oriented analysis models, which consists of an editor for the models and a system for executing these models in a formalized UML notations, and a verification system which verifies correctness of invariants attached to class diagrams. The verification system adopts HOL system for its proof engine. Second, we studied a method of converting concurrent object models into thread models. This is based on the observation that direct execution of concurrent object models obtained from object-oriented methods is not applicable to usual embedded systems where hardware and timing constraints are so severe and conventional thread style execution is mandatory. An axiom system for the conversion is obtained.

研究了形式化面向对象方法在嵌入式系统构建中的应用。首先，我们研究了构造形式化面向对象分析模型的环境，包括模型编辑器和以形式化的UML符号执行这些模型的系统，以及验证类图上附加的不变量的正确性的验证系统。验证系统采用HOL系统作为验证引擎。其次，研究了并发对象模型到线程模型的转换方法。这是基于这样的观察，即从面向对象方法获得的并发对象模型的直接执行不适用于通常的嵌入式系统，其中硬件和定时约束非常严格，并且传统的线程风格的执行是强制性的。得到了转换的公理系统。

项目成果

Toshiaki Aoki and Takuya Katayama: "Prototype Execution of Independently Constructed Object-Oriented Analysis Model"Automating the Object-Oriented Software Development Methods, ECOOP2001 Workshop. 25-33 (2001)

Toshiaki Aoki 和 Takuy​​a Katayama：“独立构建的面向对象分析模型的原型执行”自动化面向对象的软件开发方法，ECOOP2001 研讨会。

青木利晃, 立石孝彰, 片山卓也: "定理証明技術のオブジェクト指向分析への適用"コンピュータソフトウェア. 18巻4号. 18-48 (2001)

Toshiaki Aoki、Takaaki Tateishi、Takuy​​a Katayama：“定理证明技术在面向对象分析中的应用”，第 18 卷，第 4 期。18-48 (2001)。

Masumi Toyoshima: "Implementing Fault Tolerant Software In Distributed Environment"Kluwer Academic Publishers, Dependable Network Computing. 5. 341-358 (2000)

Masumi Toyoshima：“在分布式环境中实现容错软件”Kluwer 学术出版社，可靠网络计算。

Mitsutaka Okazaki, Toshiaki Aoki and Takuya Katayama: "Extracting threads from concurrent objects for the design of embedded systems"Proceedings of Asia-Pacific Software Engineering Conference APSEC2002. 107-116 (2002)

Mitsutaka Okazaki、Toshiaki Aoki 和 Takuy​​a Katayama：《从并发对象中提取线程用于嵌入式系统的设计》亚太软件工程会议 APSEC2002 论文集。

Takaaki Tateishi, Toshiaki Aoki and Takuya Katayama: "Successive Behavior Approximation Method for Verifying Distributed Objects"Third International Conference on Parallel and Distributed Computing, Applications and Technologies PDCAT2002. 439-446 (2002)

Takaaki Tateishi、Toshiaki Aoki 和 Takuy​​a Katayama：“验证分布式对象的连续行为近似方法”第三届并行和分布式计算、应用和技术国际会议 PDCAT2002。