Formal Verification of Real-Time Embedded Software for Multicore Platforms

Sagar Chaki, Arie Gurfinkel, Proceedings of the 1st Analytic Virtual Integration of Cyber-Physical Systems Workshop (AVICPS'10), pages 39-41, Nov 30, 2010

Abstract: Real-time embedded software (RTES) plays an increasingly critical role in all aspects of our lives. Ensuring that RTES behave in a predictable, safe and secure manner is an open challenge. The emergence of multicore hardware has introduced an additional level of complexity to this arena. In this paper, we take the position that formal verification is a very promising approach to find concurrency-related problems in multicore RTES. We argue that multicore RTES present unique domain-specific restrictions (and new challenge problems) that can be leveraged (and targeted) by formal verification to yield solutions that are precise, scalable, automated, and applicable to source code. We also believe that this effort will increase synergy between formal verification and real-time scheduling.

PDF