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.