Formally verifying an RTOS scheduling monitor IP core in embedded systems

The implementation of complex, high-performance functionalities in nano-CMOS technologies faces significant design and test challenges related to the need of adopting robust and efficient system validation methodologies. This aspect is particularly true for embedded systems devoted to critical applications, where human life or large amounts of economical resources are at a premium. In this work, we propose a new approach to obtain formal models that are suitable to formal equivalence checking methodologies. These checking methodologies deal with verifying the functionality of embedded systems devoted to critical applications. The main advantage of this approach is based on the fact that it makes it possible to apply a formal algorithm on the model to guarantee design bugs absence. Along with the work, a case-study is presented to demonstrate the various aspects of the proposed approach.