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 研讨会。

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

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

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

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

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 论文集。

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

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