## 3 Backward Reachability-Based Schedulability Test
### Backward Reachability-Based Case Analysis
**  
\(i>j\) and \(i>k\): \(re^{k}\preceq r^{j}_{p}\preceq re^{i}\preceq(e^{j}_{p}=f^{i}_{p})\preceq r^{i} \preceq re^{i}\preceq b^{i}\)--as Case 3--but the previous red execution state occurs after the previous green release. This case is safe. It is almost the same as the previous case, but the execution time of the red job is less than the stable period of the green-dashed lifeline. Therefore, the red release and execution cannot prevent green from executing because of the fixed priority: if the green and red tasks are ready to start jobs at the same time, the green job must start. There is no path in \(M^{T}\) that leads to such a situation. The condition for this picture is \(\exists j\
eq i:\ (C_{j}\leq D_{i}<2\cdot C_{j}\wedge C_{i}\leq D_{j}-C_{j} \wedge(\forall k\
eq j\wedge k\
eq i:\ C_{k}\geq D_{j}+C_{j}))\). Similar to the above analysis of the lifelines of red and green tasks where the blue task started before \(r^{j}_{p}\), the next four cases consider the releases of the blue task \(k\) that occur between the last two releases of the green task: \(r^{j}_{p}\preceq re^{k}\preceq re^{i}\). **Case 5. **  
\(i>j\) and \(i>k\): \(e^{k}_{p}\preceq r^{j}_{p}\preceq r^{i}\preceq e^{j}_{p}\preceq re^{k}\preceq re ^{j}\preceq b^{i}\)--as Case 2--but the last blue release occurs after the previous green execution state. This case is safe. This case repeats the reasoning for Case 2 and it is easy to see that any release position of the blue task between \(r^{j}_{p}\) and \(re^{i}\) does not affect this reasoning. The condition for this picture is \(\exists j\
eq i:\ (D_{i}\geq 2\cdot C_{j}\wedge(\forall k\
eq j\wedge k\
eq i:\ C_{k} \geq C_{j}))\). **Case 6. **  
\(i>j\) and \(i>k\): \(e^{l}\preceq r^{j}_{p}\preceq(e^{j}_{p}=f^{l})\preceq re^{k}\preceq r^{i} \preceq re^{j}\preceq b^{i}\)--as Case 3--but the last blue release occurs after the previous green execution state and before the last release of the red job. This case is unsafe, and is similar to Case 3. Here, we consider the blue release between the red release and state \(e^{j}_{p}\), after which the green job is executed. Since there are two releases after \(e^{j}_{p}\), either a red or blue task can complete their job at \(e^{j}_{p}\) to prevent the green job from starting. Again, there is a sequence of task releases from the initial state that leads to the bad state. The condition for this picture is \(\exists j\
eq i:\ (C_{j}\leq D_{i}<2\cdot C_{j}\wedge C_{i}>D_{j}-C_{j}\wedge( \forall k\
eq j\wedge k\
eq i:\ D_{i}\leq C_{k}\leq 2\cdot C_{j}))\). **Case 7. **  
\(i>j\) and \(i>k\): \(e_{p}^{i}\preceq r_{p}^{j}\preceq re^{k}\preceq(e_{p}^{j}=f_{p}^{i})\preceq r ^{i}\preceq re^{i}\preceq b^{i}\)--as Case 6--but the last blue release precedes the previous green execution state. This case is almost the same as the previous one, except that the last blue release occurs between \(r_{p}^{i}\) and \(e_{p}^{i}\). This fact obliges the red task to prevent the green one from being started, as in Case 3. As before, there is a path from the initial state that leads to the bad state. The condition for this picture is \(\exists j\
eq i:\ (C_{j}\leq D_{i}<2\cdot C_{j}\wedge C_{i}>D_{j}-C_{j}\wedge( \forall k>j:2\cdot C_{j}\leq C_{k}\leq D_{j}+C_{j}))\). **Case 8. **  
\(i>j\) and \(i>k\): \((e_{p}^{k}\sim e_{p}^{i})\preceq r_{p}^{i}\preceq(e_{p}^{j}=f_{p}^{i})\preceq r ^{i}\preceq re^{k}\preceq re^{i}\preceq b^{i}\)--as Case 7--but the last blue release follows the last release of the red job. This case is unsafe. In the previous case, we move the blue release to a position between the red release and the green last release. Due to the stability of the red dotted lifeline, the reasoning for the previous blue states is similar to the reasoning for the previous green states (Case 2). Combined with the need to prevent the green job from being executed, as in the previous cases, we again obtain a sequence of releases from the initial state that leads to a bad state.