Verification Of μC/OS-Ⅲ Task Scheduler

In recent years, embedded devices are becoming more and more popular, and the potential risks hidden in embedded software are increasingly prominent. If embedded programs with bugs are executed in key areas, it may lead to disastrous consequences. People check errors and fix them in traditional software engineering through software testing. However, software testing cannot guarantee that the programs have no defect. Based on formal logic, program verification explores another way for ensuring safety. Program verification avoids the inherent drawback rooted in software testing. In addition, it can prove some theorems.Due to the structural and functional complexity, it is difficult to formally verify a task scheduler, the main component of an operating system. The task scheduler reads and writes data from multiple system data structures. There exists a problem to specify the relationship between them. The kernel picks the task which owns the highest priority from ready list in scheduling, and then performs a context switching. The formalization should maintain the correctness of the selection of the priority and the task control block.This thesis studies the task scheduler in μC/OS-Ⅲ. After sifting core contents from its codes, we specify the properties of highest priority informally. Based on the separation logic and SCAP, we build a machine model, operational semantics, assertion languages, and inference rules. After that, assertions which specify system data structures and system properties are defined. System code can be reasoned about modularly. Finally, the properties of the task scheduler in μC/OS-Ⅲ are verified formally. The main contributions are:(1) The verification of some properties of the task scheduler of μC/OS-Ⅲ is done, including memory safety, functional correctness of partial instructions and the highest priority.(2) We build our logic system and implement the verification in Coq proof tools. The proofs provided in our work are machine checkable.