Modeling and Analysis of the Behavior of uCOS Kernel Based on CSP

This article discussed about modeling of uCOS real time operation system kernel which is widely used in embedded system field based on CSP, describing the behavior of uCOS from the higher abstract layer, to help us understand how uCOS working better, also provide foundation of further working on uCOS includes model checking and soundness verification on uCOS. This article focused on the task scheduling and the behavior of communication by semaphore, which described task scheduling mechanism of uCOS by CSP in detail and using semaphore as example to describe the task communication mechanism to give a better understanding of task scheduling and task communication of uCOS based on CSP.