Short Paper Presentation

A Technique for Verification of Race Conditions in Real-time Systems

Nagendar Telkar, Karam Chatha, Yann-Hang Lee, Gerald Gannod and Eric Wong ( Arizona State University, USA)

Real-time embedded systems can be differentiated from computation-intensive applications by their concurrent threads of control and time-dependent operations. The presence of concurrent threads acted upon by different event arrival instances makes them highly vulnerable to race conditions. The presence of race conditions introduces non-determinism in the system and alters its temporal properties. Thus, leading to potential violation of correct system behavior. Detection of race conditions in real-time systems is the focus of this paper. This paper presents a technique for detection of race conditions based on model checking. The inter-process communication mechanisms in the VxWorks environment have been designed and modeled as networks of timed automata by utilizing UPPAAL - a real-time verification tool. The various templates for the communication mechanisms have been verified for their correctness by utilizing the Timed Computation Tree Logic. The templates are then utilized to model the real-time application and verify the absence of race conditions. The paper presents examples that demonstrate the application of the proposed technique towards verification of race conditions.

Back to technical programme page