Abstract:
In real-time embedded systems, due to race conditions, synchronization order of operations to the shared variables or shared resource during the multiple tasks may be different from one execution to another. This may cause abnormal behaviors of systems. In order to detect the possible race conditions and analyze the impacts of race conditions effectively in real-time embedded systems, a formal model of execution sequences and operation events are presented according to the timing behaviors and execution characteristics of real-time embedded systems. Their characteristics are also discussed. Based on the execution sequence model, race conditions including message races and semaphore races in real-time embedded systems are described formally and precisely. And then, a new race set is presented to describe and store race conditions in systems. It includes the information of happened-before relations and race synchronization relations among the operation events which have races. With the race set generated, a race condition graph is constructed to visualize the race conditions. It is also used to predict the potential race synchronization relations of systems. The case study shows that the approach proposed can be used to analyze and predict efficiently the potential race synchronization relations as well as the different execution situations and results of real-time embedded systems.