Automatic Synthesis and Verification of Real-Time Embedded Software
■
405
are translated into guard constraints on arcs in the generated Petri nets. This set of RTPN or
CCPN is then input to QDS or EQSS, respectively, for scheduling. Details on the scheduling
procedures can be found in [6,7], and [36]. The basic strategy is to decompose each Petri net into
conflict-free components that are scheduled individually for satisfaction of memory constraints.
A conflict-free component is a reduction of a Petri net into one without any branch place. This
is EQSS. QDS applies EQSS first and then because the resulting memory satisfying schedules
may have some sequencing flexibilities, they are taken advantage of for satisfaction of temporal
constraints. Finally,