Monitoring Ada Tasking Programs Correctly

Abstract A new correctness concept, called partial-order preserving property, for event-driven execution monitoring of Ada tasking programs is presented. By using this concept, we can describe whether or not the tasking behavior of monitored Ada programs refrains from interference by monitoring actions of an event-driven execution monitor. In this paper, we define the equivalence of dynamic concurrent structures with respect to Ada program transformation, and propose this equivalence as a partial-order preserving criterion of the $pro$gram transformation used in a preprocessor of an event-driven execution monitor of Ada tasking programs. The equivalence is formally based on the lattice of dynamic concurrent structure of Ada programs which provides an abstraction of the tasking behavior ofAda programs in terms of task interactions. 1