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

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

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.