The adaptation of an operatingsystem to an application is often needed to optimize the embedded code. Adaptation consists in removing the unneeded operatingsystems services and the dead code according to application...
详细信息
ISBN:
(纸本)9781479989379
The adaptation of an operatingsystem to an application is often needed to optimize the embedded code. Adaptation consists in removing the unneeded operatingsystems services and the dead code according to applications requirements. The resulting stripped operatingsystem 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 operatingsystem 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 operatingsystem, a formal model is used. All the functions of the operatingsystem 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.
暂无评论