Embedded systems are increasingly employed in safety-critical situations and the presence of bugs has serious consequences. Verifying safety properties of such systems is a step towards proving their correctness. Analysing embedded systems is challenging due to the use non-standard synchronization mechanisms like disabling and enabling of interrupts, suspending and resuming of scheduler or specific threads, dynamically raising and lowering thread priorities, use of flags, etc. in addition to the standard locks. I strive to come up with a principled approach to statically analyse such systems.
I have worked on a range of real time kernels that include FreeRTOS kernel (from Real Time Engineers Ltd.), TI-RTOS (Texas Instruments), ChibiOS (Giovanni Di Sirio), and P-RTOS (from an Indian aeronautics major) and applications like ArduPilot, Android apps, nxtOSEK programs, and LEGO-OSEK programs. I have developed tools in OCaml to statically analyze these systems.