Upload New File

Firebird_Pre_loaded_examples/Example45_Martian_Lander.mp

+/* 	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;