diff --git a/Firebird_Pre_loaded_examples/Example45_Martian_Lander.mp b/Firebird_Pre_loaded_examples/Example45_Martian_Lander.mp new file mode 100644 index 0000000000000000000000000000000000000000..10b3b3a4fc8ad6e14215d21f31e284fd1b61b052 --- /dev/null +++ b/Firebird_Pre_loaded_examples/Example45_Martian_Lander.mp @@ -0,0 +1,163 @@ +/* Example 45. Real time system behavior modeling. + Landing system for Martian Lander. + + MP model written by M.Auguston following example 1 and Appendix B from + Farnam Jahanian, Aloysius Ka-Lau Mok + "Safety analysis of timing properties in real-time systems", + IEEE Transactions on Software Engineering + Year: 1986, Volume SE-12, Issue 9, pp.890-904 + +The landing system operates in one of two modes: normal or emergency. +When the system is turned on (an external event), it operates in the +normal mode. While in the normal landing mode, the pilot can control +acceleration, velocity, and position by adjusting the downward thrust +generated by the rocket motor, thus bringing the space vehicle to a +safe landing. This task is continually performed in two phases. + +In phase 1, an I/O device is started to read the acceleration set +by the pilot, and a hardware timer is started which generates a timer +interrupt (i.e., external event TMRINT) after 100 ms. In phase 2, +when the I/O operation is completed (i.e., external event IOINT), +the motor thrust is adjusted appropriately. However, if for some +reason the I/O operation is not done within 100 ms, the timer interrupt +initiates the emergency landing mode. While in the emergency mode, +the altitude and velocity is periodically sampled and a retro-rocket +is automatically fired to bring the vehicle to a safe landing. + +Events and actions: +RACC Starts IO device to read acceleration +STMR Start hardware watchdog timer, this model has two timers +ADJM Adjust motor thrust +TDP Transmit info to display panel +IEM Initiate emergency mode +ETC Other housekeeping function, +IVEL Input measured velocity +IALT Input measured altitude +CKDT Check input data for consistency +RRM Retro-rocket module +START Systems start up, +IOINT I/O device signals completion +TMRINT Timer Interrupt, occurs at least 100 ms after start of STMR + +Action Time in ms +RACC 10 +STMR 10 +ADJM 20 +TDP 10 +IEM 10 +ETC 10 +IVEL 20 +IALT 20 +CKDT 10 +RRM 10 + + run for scope 1 and up. +*/ +SCHEMA Martian_Lander + +ROOT Measure_and_display: + /* runs Timer1 */ + STMR1 + (+ {IVEL, IALT} + CKDT + TDP + +) + stop_Timer1 +; + +ROOT Landing: + START +/* Phase 1 */ + { RACC, + STMR1, /* starts Timer1 */ + STMR2 /* starts Timer2 */ + } + + (+ { ADJM, ETC } +) + +/* Phase 2 */ + (IOINT | /* normal landing */ + + TMRINT /* Timer2 sets interrupt */ + IEM /* initiate emergency mode */ + Emergency_Landing ) + + Lands + {stop_Timer1, stop_Timer2} +; + +Emergency_Landing: + (* fire_RRM *) +; + +ROOT Timer2: +/* responsible for switching on Emergency_landing after 100 msec */ + STMR2 + [ TMRINT ] + stop_Timer2 +; + +Landing, Measure_and_display SHARE ALL STMR1, stop_Timer1; +Landing, Timer2 SHARE ALL STMR2, TMRINT, stop_Timer2; + +/*=== set timing for events, in ms ===*/ +COORDINATE $a: RACC DO SET $a.duration AT LEAST 10; OD; +COORDINATE $a: STMR1 DO SET $a.duration AT LEAST 10; OD; +COORDINATE $a: STMR2 DO SET $a.duration AT LEAST 10; OD; +COORDINATE $a: ADJM DO SET $a.duration AT LEAST 20; OD; +COORDINATE $a: TDP DO SET $a.duration AT LEAST 10; OD; +COORDINATE $a: IEM DO SET $a.duration AT LEAST 10; OD; +COORDINATE $a: ETC DO SET $a.duration AT LEAST 10; OD; +COORDINATE $a: IVEL DO SET $a.duration AT LEAST 20; OD; +COORDINATE $a: IALT DO SET $a.duration AT LEAST 20; OD; +COORDINATE $a: CKDT DO SET $a.duration AT LEAST 10; OD; +COORDINATE $a: fire_RRM DO SET $a.duration AT LEAST 10; OD; + +/*=== arrange trace annotations ===*/ +ADD SAY("Running Timer1") alert Measure_and_display; + +COORDINATE $a: TMRINT DO + SET $a.start AT LEAST 101; + ADD SAY("Emergency landing started at " $a.start) alert $a; +OD; + +COORDINATE $a: Lands DO + ADD SAY("Landing complete at " $a.end) alert $a; +OD; + +/* measurement and display continue till the landing is complete */ +ENSURE FOREACH $a: IVEL (Measure_and_display.start - $a.start) >= 40 -> + EXISTS $b: IVEL $a PRECEDES $b; + +/*====== main timing constraint ======*/ +/* normal landing completes before the deadline 100 msec. */ +ENSURE FOREACH $a: IOINT $a.start <= 100; + +/*===== table for some event timings =====*/ +TABLE Time_table{ TITLE("Event timings"); + TABS string event_name, number start_time, + number event_duration, number end_time; + }; + +CLEAR Time_table; /* prepare for the new event trace */ + +/* pick up timing for some events */ +COORDINATE $x: (IVEL | IALT | TDP | ADJM | fire_RRM | + Emergency_Landing | Lands | stop_Timer1) DO + Time_table <| event_name: SAY($x), + start_time: $x.start.smallest, + event_duration: $x.duration.smallest, + end_time: $x.end.smallest; +OD; + +SHOW Time_table; + +/* show Gantt Chart for some event timing */ +BAR CHART Timing{ TITLE("Event timings"); + FROM Time_table; + X_AXIS event_name; + TABS start_time, event_duration; /* show these values only */ + ROTATE; /* show as Gantt chart */ +}; + +SHOW Timing;