Static verification of task access to shared resources in real-time systems

Among issues which arise when developing software complexes for real-time systems (RTS) one should resolve common multi-task system issues of ensuring logical correctness of the system being created (preserving the integrity of informational resources, eliminating the possibility of mutual task blocking), as well as issues of ensuring dynamic correctness, specific for RTS (feasibility of the application tasks). In the long run, resolving these issues is reduced to checking the correctness of how synchronizing operators which ensure consistent execution of application tasks are scattered in the task bodies. In order to perform such checking statically, models which represent the scattering of synchronizing operators in application tasks are constructed.
In this paper several methods of processing such models are proposed which are based on constructing special multi-partite graphs — graphs of synchronizing operator dependencies. Two varieties of such graphs are resented: a) graphs of bundles, which ensure verification of logical correctness of multi-task applications (correctness of intersections of critical interval pairs); and b) graphs of bundles and critical intervals, which ensure verification of dynamic correctness of RTS applications.