(******************************************************************************* * IMITATOR MODEL * * Title : FMTV_2 * Description : * Correctness : * Scalable : * Generated : * Categories : Industrial ; Protocol ; RTS * Source : * bibkey : SAL15 * Author : G. Lipari and Youcheng Sun * Modeling : * Input by : * License : * * Created : 2015/xx/xx (< 2015/10/30) * Last modified : 2020/08/18 * Model version : * * IMITATOR version : 3 ******************************************************************************) var (** CONSTANTS **) P6 = 100, J6 = 20, (*the jitter of task 6*) C6_seg1_max = 4, C6_seg1_min = 4, C6_seg2_max = 10, C6_seg2_min = 9, C6_seg3_max = 5, C6_seg3_min = 4, C5_min = 4, C5_max = 7, C7_min = 11, C7_max = 14, P2 = 40, C2_min = 17, C2_max = 17, : parameter; (** CLOCKS **) sched_urgent, j6, p6, c6, p5, c5, p7, c7, p2, c2, delay : clock; (* PARAMETERS *) P2_delta = 0.04, P2_uncertain, (* The latency of the chain T5-T7 *) D : parameter; (** Task T6 **) automaton T6 synclabs: T6_arr, T6_start, T6_dis, T6_pre, T6_act, T7_act, T5_act, T6_end, miss_event; loc T6_idle: invariant p6 <= P6 (*ing for activation *) when p6 = P6 do {p6 := 0, j6 := 0, delay := 0} goto T6_jitter_pre; loc T6_jitter_pre: invariant j6 <= J6 (*ing for jitter*) when j6 <= J6 sync T6_arr do {c6 := 0} goto T6_jitter_post; loc T6_jitter_post: invariant c6 <=0 (*signal the start*) when c6 = 0 sync T6_start do {c6 := 0} goto T6_seg1_susp; loc T6_seg1_susp: invariant p6<=P6 stop {c6} (*the task is suspended*) when True sync T6_dis goto T6_seg1_exec; when p6=P6 (*signal a deadline miss*) sync miss_event do {p6 := 0} goto T6_idle; loc T6_seg1_exec: invariant c6<=C6_seg1_max (*T6 executes*) when c6 >= C6_seg1_min sync T5_act do {c6 := 0} goto T6_hole_pre; when p6 >= P6 (*dline miss*) sync miss_event do {p6 := 0} goto T6_idle; when True (*preemption*) sync T6_pre goto T6_seg1_susp; loc T6_hole_pre: invariant c6 <= 0 (*signal "end of seg1"*) when c6 = 0 sync T6_end goto T6_hole; (*-- loc T6_hole_act: invariant c6 <= 0 (*activates T5*) -- when c6 = 0 -- sync T5_act -- -- goto T6_hole;*) loc T6_hole : invariant True (*s for end of T5 *) when True sync T6_act do {c6 := 0} goto T6_hole_post; loc T6_hole_post : invariant c6 <= 0 (*signal a fake arrival time*) when c6=0 sync T6_arr do {c6 := 0} goto T6_seg2_susp; loc T6_seg2_susp: invariant p6 <= P6 stop {c6} (*suspended invarianting for a schedule dispatch event*) when True sync T6_dis goto T6_seg2_exec; when p6=P6 (*miss ? *) sync miss_event do {p6 := 0} goto T6_idle; loc T6_seg2_exec: invariant c6<=C6_seg2_max (*executes the second segment*) when c6 >= C6_seg2_min sync T7_act do {c6 := 0} goto T6_seg3_exec; when p6 >= P6 (*miss ?*) sync miss_event do {p6 := 0} goto T6_idle; when True (*preemption*) sync T6_pre goto T6_seg2_susp; loc T6_seg3_exec: invariant c6<=C6_seg3_max (*executes the third segment*) when c6 >= C6_seg3_min (*T6 completed*) sync T6_end do {c6 := 0} goto T6_idle; when p6 >= P6 (*miss ?*) sync miss_event do {p6 := 0} goto T6_idle; when True (*preemption*) sync T6_pre goto T6_seg3_susp; loc T6_seg3_susp: invariant p6 <= P6 stop {c6} (*suspended invarianting for a schedule dispatch event*) when True sync T6_dis goto T6_seg3_exec; when p6=P6 (*miss ? *) sync miss_event do {p6 := 0} goto T6_idle; end (** Task T5 **) automaton T5 synclabs: T5_arr, T5_end, T5_pre, T5_dis, T5_act, T6_act; loc T5_idle: invariant True when True sync T5_act do {c5 := 0} goto T5_starting; loc T5_starting: invariant c5 <= 0 when c5 = 0 sync T5_arr goto T5_susp; loc T5_susp: invariant True stop {c5} when True sync T5_dis goto T5_exec; loc T5_exec: invariant c5 <= C5_max when c5 >= C5_min sync T5_end do {c5 := 0} goto T5_ending; when True sync T5_pre goto T5_susp; loc T5_ending: invariant c5<=0 when c5 = 0 sync T6_act goto T5_idle; end (* Task T7 *) automaton T7 synclabs: T7_act, T7_arr, T7_end, T7_dis, T7_pre, T7_finish; loc T7_idle: invariant True when True sync T7_act do { c7 := 0 } goto T7_starting; loc T7_starting: invariant c7 <=0 when c7 = 0 sync T7_arr do { c7 := 0 } goto T7_susp; loc T7_susp: invariant True stop {c7} when True sync T7_dis goto T7_exec; loc T7_exec: invariant c7<=C7_max when c7 > C7_min sync T7_finish do {c7 := 0} goto T7_ending; when True sync T7_pre goto T7_susp; loc T7_ending: invariant c7<=0 when c7 = 0 sync T7_end goto T7_idle; end (* AUTOMATON T2 *) automaton T2 synclabs: T2_arr, T2_dis, T2_pre, T2_end; loc T2_idle: invariant p2 <= P2_uncertain when p2 = P2_uncertain sync T2_arr do {p2 := 0, c2 := 0} goto T2_susp; loc T2_susp: invariant True stop {c2} when True sync T2_dis goto T2_exec; loc T2_exec: invariant c2 <= C2_max when c2 >= C2_min sync T2_end goto T2_idle; when True sync T2_pre goto T2_susp; end (* Observer Automaton *) automaton Observer synclabs: miss_event, T6_start, T7_finish; loc Obs_idle: invariant True when True sync T6_start (* delay := 0} *) goto Obs_start; when True sync miss_event goto Obs_miss; loc Obs_start: invariant True when delay = D sync T7_finish goto Obs_stop; loc Obs_stop: invariant True when True do{} goto Obs_stop; loc Obs_miss: invariant True when True goto Obs_miss; end (* SCHEDULER AUTOMATON *) automaton sched_sched synclabs : T2_arr, T2_dis, T2_pre, T2_end, T6_arr, T6_dis, T6_pre, T6_end, T5_arr, T5_dis, T5_pre, T5_end, T7_arr, T7_dis, T7_pre, T7_end; loc sched_loc_ : invariant True when True sync T2_arr do {sched_urgent := 0} goto sched_loc_AT2; when True sync T6_arr do {sched_urgent := 0} goto sched_loc_AT6; when True sync T5_arr do {sched_urgent := 0} goto sched_loc_AT5; when True sync T7_arr do {sched_urgent := 0} goto sched_loc_AT7; loc sched_loc_AT2 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T2_dis goto sched_loc_RT2; loc sched_loc_AT6 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_dis goto sched_loc_RT6; loc sched_loc_AT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_dis goto sched_loc_RT5; loc sched_loc_AT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T7_dis goto sched_loc_RT7; loc sched_loc_RT7 : invariant True when True sync T2_arr do {sched_urgent := 0} goto sched_loc_AT2RT7; when True sync T6_arr do {sched_urgent := 0} goto sched_loc_AT6RT7; when True sync T5_arr do {sched_urgent := 0} goto sched_loc_AT5RT7; when True sync T7_end do { sched_urgent := 0 } goto sched_loc_ET7; loc sched_loc_ET7 : invariant sched_urgent <= 0 when sched_urgent = 0 goto sched_loc_; loc sched_loc_AT2RT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T7_pre goto sched_loc_AT2WT7; loc sched_loc_AT2WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T2_dis goto sched_loc_RT2WT7; loc sched_loc_AT6RT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T7_pre goto sched_loc_AT6WT7; loc sched_loc_AT6WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_dis goto sched_loc_RT6WT7; loc sched_loc_AT5RT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T7_pre goto sched_loc_AT5WT7; loc sched_loc_AT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_dis goto sched_loc_RT5WT7; loc sched_loc_RT5 : invariant True when True sync T2_arr do {sched_urgent := 0} goto sched_loc_AT2RT5; when True sync T6_arr do {sched_urgent := 0} goto sched_loc_AT6RT5; when True sync T7_arr do {sched_urgent := 0} goto sched_loc_RT5WT7; when True sync T5_end do { sched_urgent := 0 } goto sched_loc_ET5; loc sched_loc_ET5 : invariant sched_urgent <= 0 when sched_urgent = 0 goto sched_loc_; loc sched_loc_AT2RT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_pre goto sched_loc_AT2WT5; loc sched_loc_AT2WT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T2_dis goto sched_loc_RT2WT5; loc sched_loc_AT6RT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_pre goto sched_loc_AT6WT5; loc sched_loc_AT6WT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_dis goto sched_loc_RT6WT5; loc sched_loc_RT5WT7 : invariant True when True sync T2_arr do {sched_urgent := 0} goto sched_loc_AT2RT5WT7; when True sync T6_arr do {sched_urgent := 0} goto sched_loc_AT6RT5WT7; when True sync T5_end do { sched_urgent := 0 } goto sched_loc_ET5WT7; loc sched_loc_ET5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T7_dis goto sched_loc_RT7; loc sched_loc_AT2RT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_pre goto sched_loc_AT2WT5WT7; loc sched_loc_AT2WT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T2_dis goto sched_loc_RT2WT5WT7; loc sched_loc_AT6RT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_pre goto sched_loc_AT6WT5WT7; loc sched_loc_AT6WT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_dis goto sched_loc_RT6WT5WT7; loc sched_loc_RT6 : invariant True when True sync T2_arr do {sched_urgent := 0} goto sched_loc_AT2RT6; when True sync T5_arr do {sched_urgent := 0} goto sched_loc_RT6WT5; when True sync T7_arr do {sched_urgent := 0} goto sched_loc_RT6WT7; when True sync T6_end do { sched_urgent := 0 } goto sched_loc_ET6; loc sched_loc_ET6 : invariant sched_urgent <= 0 when sched_urgent = 0 goto sched_loc_; loc sched_loc_AT2RT6 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_pre goto sched_loc_AT2WT6; loc sched_loc_AT2WT6 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T2_dis goto sched_loc_RT2WT6; loc sched_loc_RT6WT7 : invariant True when True sync T2_arr do {sched_urgent := 0} goto sched_loc_AT2RT6WT7; when True sync T5_arr do {sched_urgent := 0} goto sched_loc_RT6WT5WT7; when True sync T6_end do { sched_urgent := 0 } goto sched_loc_ET6WT7; loc sched_loc_ET6WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T7_dis goto sched_loc_RT7; loc sched_loc_AT2RT6WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_pre goto sched_loc_AT2WT6WT7; loc sched_loc_AT2WT6WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T2_dis goto sched_loc_RT2WT6WT7; loc sched_loc_RT6WT5 : invariant True when True sync T2_arr do {sched_urgent := 0} goto sched_loc_AT2RT6WT5; when True sync T7_arr do {sched_urgent := 0} goto sched_loc_RT6WT5WT7; when True sync T6_end do { sched_urgent := 0 } goto sched_loc_ET6WT5; loc sched_loc_ET6WT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_dis goto sched_loc_RT5; loc sched_loc_AT2RT6WT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_pre goto sched_loc_AT2WT6WT5; loc sched_loc_AT2WT6WT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T2_dis goto sched_loc_RT2WT6WT5; loc sched_loc_RT6WT5WT7 : invariant True when True sync T2_arr do {sched_urgent := 0} goto sched_loc_AT2RT6WT5WT7; when True sync T6_end do { sched_urgent := 0 } goto sched_loc_ET6WT5WT7; loc sched_loc_ET6WT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_dis goto sched_loc_RT5WT7; loc sched_loc_AT2RT6WT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_pre goto sched_loc_AT2WT6WT5WT7; loc sched_loc_AT2WT6WT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T2_dis goto sched_loc_RT2WT6WT5WT7; loc sched_loc_RT2 : invariant True when True sync T6_arr do {sched_urgent := 0} goto sched_loc_RT2WT6; when True sync T5_arr do {sched_urgent := 0} goto sched_loc_RT2WT5; when True sync T7_arr do {sched_urgent := 0} goto sched_loc_RT2WT7; when True sync T2_end do { sched_urgent := 0 } goto sched_loc_ET2; loc sched_loc_ET2 : invariant sched_urgent <= 0 when sched_urgent = 0 goto sched_loc_; loc sched_loc_RT2WT7 : invariant True when True sync T6_arr do {sched_urgent := 0} goto sched_loc_RT2WT6WT7; when True sync T5_arr do {sched_urgent := 0} goto sched_loc_RT2WT5WT7; when True sync T2_end do { sched_urgent := 0 } goto sched_loc_ET2WT7; loc sched_loc_ET2WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T7_dis goto sched_loc_RT7; loc sched_loc_RT2WT5 : invariant True when True sync T6_arr do {sched_urgent := 0} goto sched_loc_RT2WT6WT5; when True sync T7_arr do {sched_urgent := 0} goto sched_loc_RT2WT5WT7; when True sync T2_end do { sched_urgent := 0 } goto sched_loc_ET2WT5; loc sched_loc_ET2WT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_dis goto sched_loc_RT5; loc sched_loc_RT2WT5WT7 : invariant True when True sync T6_arr do {sched_urgent := 0} goto sched_loc_RT2WT6WT5WT7; when True sync T2_end do { sched_urgent := 0 } goto sched_loc_ET2WT5WT7; loc sched_loc_ET2WT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T5_dis goto sched_loc_RT5WT7; loc sched_loc_RT2WT6 : invariant True when True sync T5_arr do {sched_urgent := 0} goto sched_loc_RT2WT6WT5; when True sync T7_arr do {sched_urgent := 0} goto sched_loc_RT2WT6WT7; when True sync T2_end do { sched_urgent := 0 } goto sched_loc_ET2WT6; loc sched_loc_ET2WT6 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_dis goto sched_loc_RT6; loc sched_loc_RT2WT6WT7 : invariant True when True sync T5_arr do {sched_urgent := 0} goto sched_loc_RT2WT6WT5WT7; when True sync T2_end do { sched_urgent := 0 } goto sched_loc_ET2WT6WT7; loc sched_loc_ET2WT6WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_dis goto sched_loc_RT6WT7; loc sched_loc_RT2WT6WT5 : invariant True when True sync T7_arr do {sched_urgent := 0} goto sched_loc_RT2WT6WT5WT7; when True sync T2_end do { sched_urgent := 0 } goto sched_loc_ET2WT6WT5; loc sched_loc_ET2WT6WT5 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_dis goto sched_loc_RT6WT5; loc sched_loc_RT2WT6WT5WT7 : invariant True when True sync T2_end do { sched_urgent := 0 } goto sched_loc_ET2WT6WT5WT7; loc sched_loc_ET2WT6WT5WT7 : invariant sched_urgent <= 0 when sched_urgent = 0 sync T6_dis goto sched_loc_RT6WT5WT7; loc sched_loc_stop : invariant True end (************************************************************) (* Initial state *) (************************************************************) init := (*------------------------------------------------------------*) (* Initial location *) (*------------------------------------------------------------*) (* Init scheduler *) & loc[sched_sched] = sched_loc_ & sched_urgent = 0 (* Init T6 *) & loc[T6] = T6_idle & c6 = 0 & j6 = 0 & p6 >= 0 & p6 <= P6 (* Init T5 *) & loc[T5] = T5_idle & c5 = 0 (* Init T7 *) & loc[T7] = T7_idle & c7 = 0 (* Init T2 *) & loc[T2] = T2_idle & c2 = 0 & P2_uncertain-28 <= p2 & p2 <= P2_uncertain (* & 0 <= p2 & p2 <= P2_uncertain *) & P2 - P2_delta <= P2_uncertain & P2_uncertain <= P2 + P2_delta (* Init Observer *) & loc[Observer] = Obs_idle & delay = 0 & D >= 0 ; (************************************************************) (* The end *) (************************************************************) end