Space Shuttle Requirements

Users of the SDAP are cautioned that, at very small rate limits and deadbands, e.g., 0.01 deg/s and 0.01 deg for vernier jets, simulation results using the models presented here may not represent real vehicle behavior because of the model simplifications.

Do we have to do anything. Like check that rate limits and deadband should be above the thresholds?

General. Do know exactly where to define it.

The conditioning inputs shown in Figure 2 include DAP parameters, such as attitude rate limits and deadbands and other quantities that the crew can set via keyboard entry, and by push-button moding discretes, such as the choices between primary and vernier jets and automatic and manual attitude control.

Is this really a requirement?

When the steering mode is manual open-loop, the State Error and Phase Plane modules can be bypassed; jets are fired directly by moving the rotational hand controller (RHC) out of detent.

This property is general and describe how the flow of values is propagated. The Figure 3 describe the general flow.

General. Shall be expressed within SDAP since the use of StateError of PhasePlace are not visible from outside.

If in AUTO, the desired state comes from the auto maneuver logic

if in MANUAL, the desired state depends on the hand controller history

The flight code pulse mode can be emulated by an appropriate choice of RHC deflection interval

In flight, pulse sizes in all axes are controlled by a single crew specified rate change quantity which is divided by an estimated per axis acceleration to compute pulse duration

Pulses in close proximity to one another generally will all be based on one rate change value

In any one axis, plus and minus pulses will be of the same duration

SDAP Executive routine calls the SDAP modules in proper sequence

SDAP Executive routine sets SDAP moding flags

A clock is maintained that increments time at intervals of 80 ms, the SDAP time step

If the hand controller is deflected in any axis, the SDAP automatically switches to manual mode

(* Req Id: req_s3_1_2_2_p19_1

   Text:  If the hand controller is deflected in any axis, 
			the SDAP automatically switches to manual mode 

   Comment: no comment

   Origin: Section 3.1 SDAP Executive, p19 

   Scope: SDAP_Exec_Prop(   -- inputs
	    auto_manual_switch: bool;
	    bypass_in: bool^3;
	    rhc_state: int^3; -- only 0, +/-1
	    ) returns (     -- outputs
	    bypass_out: bool^3;
	    initialize_auto_maneuver: bool;
	    initialize_jet_selection: bool;
	    initialize_state_error: bool;
	    );

	Simulink Component Name: UpdateAutoManualSwitch.slx
	Req Contract PATH: UpdateAutoManualSwitch/Req_s3_1_2_2_p19_1
*)
contract req_s3_1_2_2_p19_1 ( -- inputs
	   rhc_state: int^3;
	   ) returns (       -- outputs
	   auto_manual_switch: bool;
	   );
let
	guarantees (rhc_state[1] <> 0 or rhc_state[2] <>0 or rhc_state[3] <> 0) => not auto_manual_switch;
tel	   

On the first pass, the jet select initialization flag is set

On the first pass, if the mode is manual, the state error initialization flag is set

Every second pass, the Attitude Processor and Part 1 of the State Estimator are called to incorporate new attitude information from the IMU.

When the maneuver mode is changed from manual to auto, if the bypass flag is ON, it is set to OFF and the auto maneuver initialization flag is set to ON.

(* Req Id: req_s3_1_2_2_p19_5

   Text: When the maneuver mode is changed from manual to auto, if the bypass
	 flag is ON, it is set to OFF and the auto maneuver
	 initialization flag is set to ON.

	Comment: initialization flag is set to ON, but will be set to OFF at the end of AUTO MANEUVER in the same timestep.
	So Basically, checking this initialization has been checked in the Simulink Model.

   Comment: no comment

   Origin: Section 3.1 SDAP Executive, p19 

   Scope: SDAP_Exec_Prop(   -- inputs
	    auto_manual_switch: bool;
	    bypass_in: bool^3;
	    rhc_state: int^3; -- only 0, +/-1
	    ) returns (     -- outputs
	    bypass_out: bool^3;
	    initialize_auto_maneuver: bool;
	    initialize_jet_selection: bool;
	    initialize_state_error: bool;
	    );

	Simulink Component Name: AutoManualManeuver.slx
*)
contract req_s3_1_2_2_p19_5 ( -- inputs
	   auto_manual_switch: bool;
	   bypass_in: bool^3;
	   ) returns (       -- outputs
	   bypass_out: bool^3;
	   );
let

-- Req_s3_1_2_2_p19_5 is refined into 3 sub-properties, one for each dimension
-- Local Variables
-- switching from manual to auto 
var manual_to_auto : bool = not (pre auto_manual_switch) and auto_manual_switch;
var req_s3_1_2_2_p19_5_1 : bool =
   manual_to_auto and bypass_in[1] => not bypass_out[1];
var req_s3_1_2_2_p19_5_2 : bool =
   manual_to_auto and bypass_in[2] => not bypass_out[2];
var req_s3_1_2_2_p19_5_3 : bool =
   manual_to_auto and bypass_in[3] => not bypass_out[3];


guarantees req_s3_1_2_2_p19_5_1;
guarantees req_s3_1_2_2_p19_5_2;
guarantees req_s3_1_2_2_p19_5_3;
tel	   

Since the Auto Maneuver module is processed at 1.04 Hz, it is called every 12th DAP pass whenever SDAP is in the auto mode.

If the mode is manual, the Manual Maneuver module is called each SDAP pass.

If any of the bypass-flag elements are OFF, then Phase Plane is called to set the rotation commands in those axes.

The Attitude Processor module is called every second SDAP pass; that is, on the same pass on which Part 1 of the State Estimator is called

if this attitude is sufficiently different from the current attitude, the SDAP executes a maneuver at a preselected maneuver rate until the current attitude approaches the commanded attitude

Auto Maneuver tests the rotation angle \(\Delta\theta\) against two numerical criteria. If \(\Delta\theta\) is larger than \(y\), the module places itself in the maneuver mode; if \(\Delta\theta\) is less than \(x\), the hold mode results.

DESIRED RATE is either zero during hold or the projection of MANEUVER RATE on the eigen axis during maneuver.

In the hold mode, DESIRED ATTITUDE is the attitude estimate plus the projection of the rotation angle \(\Delta\theta\) the eigen axis

When the maneuver mode is first entered, DESIRED ATTITUDE is set equal to the current attitude estimate plus a bias vector. The State Error module then has an attitude error equal to the bias vector.

On each pass, State Error adds an attitude increment of \(0.08 \cdot \text{DESIRED RATE}\) to the desired attitude so that the attitude error is always referred to a frame rotating at the desired maneuver rate.

The open-loop submode issues a rotation command whenever the RHC is deflected.

The user can simulate acceleration and pulse actions by choosing an appropriate RHC deflection interval. In this submode, the module sets a BYPASS discrete and consequently, the Phase Plane module output is ignored. The rotation command is sent directly to the Jet Selection module

The closed-loop submode causes a DESIRED RATE value to be sent to State Error. For each axis in which the RHC is deflected, this rate is set equal to the input MANEUVER RATE.

When the RHC is returned to detent, the DESIRED RATE is set to zero and attitude hold is established at the current attitude.

When the closed-loop submode is operating, the Manual Maneuver module issues an INITIALIZE STATE ERROR discrete whenever a change occurs in RHC state. This allows an attitude hold to be effected at the attitude attained when the RHC is returned to detent, by zeroing the attitude error.

A FORCE FIRE discrete is sent to the Phase Plane module when the RHC is deflected (first pass of deflection only). This discrete causes at least a minimum-impulse jet firing at the beginning of RHC deflection and improves the crew "feel" of vehicle response to manual input for SDAP settings involving a large RATE LIMIT and small MANEUVER RATE.

Is it a single req or multiple ones?

The choice between manual open- and closed-loop functions is made by setting the discrete CLOSED LOOP. The ON setting selects the closed-loop function.

The desired rate equals the MANEUVER RATE when the SDAP is in the discrete rate mode and the RHC is deflected, or it equals the eigen axis projection of MANEUVER RATE when the SDAP is in the auto maneuver mode and maneuvering. Otherwise the desired rate is zero.

check completeness of the conditions

While maneuvering in the automatic maneuver mode, and while in the manual closed-loop mode with RHC deflected, desired attitude equals a snapshot of the attitude estimate at the beginning of the maneuver plus an accumulation of angular increments each equal to 0.08 times DESIRED RATE.

When the momentary INITIALIZE STATE ERROR flag is ON, DESIRED ATTITUDE is set equal to the current attitude estimate. The flag is set in the Manual Maneuver module when a change of RHC state occurs.

Crossing a switch line usually requires redetermination of jet command status. The command status is decided by determining the current state region shown in Table 22 and the required action shown in Table 23.

Encode the logic of Tables 22 and 23

At any time, for each axis, the rigid vehicle state is defined by an attitude and rate error point that must lie in one of the defined regions since the regions cover the entire plane

check that exactly one mode is selected

Regions 1 and 5 always command jets

For primary jet use, regions 2, 3, 6, and 7 always permit coast with no jet commands

Region 9 never causes commands to be generated, but a preference for vernier jet selection is computed.

Regions 4 and 8 have hysteresis. If the phase is in either region 4 or 8 and a firing is taking place (because, for example, regions 4 or 8 have been entered from regions 1 or 5), then the firing will continue until the phase point crosses the S13 switch curve. At that point, the ROTATION COMMAND magnitude will become less than one and stop the firing.

When inside region 4 or 8, after S13 has been crossed once, the ROTATION COMMAND magnitude will be less than unity since \(|S13| \leq |RL|\). In fact, it will be less than 0.8 because of the 0.8 multiplication factor. When no ROTATION COMMANDS are issued, vernier jet preferences usually are computed.

BYPASS flag effectively eliminates the Phase Plane from the SDAP by ignoring its output in favor of the RHC-commanded rotation from the Manual (open-loop) Maneuver module.

The FORCE FIRE flag initiates a firing if a command was not being set by Phase Plane when the RHC changed state in the closed-loop Manual Maneuver module.

The ROTATION COMMAND from the past cycle is input to be used in the region logic.

Is it related to Req.s3.7.2.p56.2 or an independent property ?

The two types of thrusters may not be used simultaneously

Moding between primary and vernier jets is accomplished by choosing a value for the discrete PRIMARY VERNIER SW (a simulation input).