Research on the verification of highly parallel and concurrent embedded software

我们主要研究由实时操作系统（RTOS）和实时操作系统本身控制的并行/并发软件。我们提出了一种算法和工具来验证并行/并发软件的行为，其中包含RTOS调度和前者的实时调度。对于后者，我们提出了一种验证RTOS设计和实现的方法和工具。此外，我们还将这些方法和工具应用到RTOS产品中。我们成功地在实际环境中提出了基于模型检查的验证方法，并使其适用于实际的软件产品。

We focus on parallel/concurrent software which is controlled by real-time operating system(RTOS) and RTOS itself. We have proposed an algorithm and tool to verify the behavior of parallel/concurrent software which contains scheduling by RTOS and real-time for the former. For the latter, we have proposed a method and tools to verify the design and implementation of RTOS. In addition, we have applied those method and tools to RTOS products. We succeeded in proposing verification methods based on model checking in practical settings and conducted that they are applicable to practical software products.