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.