Formal Synthesis of Optimal RTOS

The adaptation of an operating system to an application is often needed to optimize the embedded code. Adaptation consists in removing the unneeded operating systems services and the dead code according to applications requirements. The resulting stripped operating system is smaller, safer and has better performance. This adaptation is usually done by hand for each application. As a result some dead code may remain unnoticed. The verification and the certification of the adapted operating system is difficult too: for each adaptation to an application, the certification must be redone and for the verification, a new model has to be designed with the well known gap problem between the model and the actual software. In this paper, we present a new approach based on formal methods to synthesize an Application-Specific Real-Time Operating System. Instead of removing services from the source code of an existing operating system, a formal model is used. All the functions of the operating system with the full control flow and control variables are modeled. According to an application model, unneeded services and part of control flow are removed from the model by using a reachability analysis. This guarantees no dead code remains. Moreover some properties may be checked on the pruned model to ensure the application behaves as expected. At last, the corresponding source code is generated from the model.