Formal verification of software for an embedded operating system

In this work an approach is shown, how to verify embedded system applications written for the operating system Contiki using Model Checking. The used approach models the environment of the embedded system at the level of the operating system drivers. Using this approach it is possible to use a Bounded Model Checking Tool to verify applications without changing the application.