%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% The following PVS theories comprise a formal model of a subset %% of the control system functional requirements for an EVA %% propulsion system. This example is heavily based on NASA's %% Simplified Aid for EVA Rescue (SAFER), developed at the Johnson %% Space Center (JSC). For pedagogical reasons, the requirements %% deviate somewhat from the actual SAFER system. Furthermore, the %% SAFER system is still under development. As a result, the model %% that follows does not necessarily reflect the actual SAFER %% requirements as maintained by JSC. %% %% References: %% 1. Simplified Aid for EVA Rescue (SAFER) Operations Manual. %% NASA report JSC-26283, Sept. 1994. %% 2. Simplified Aid for EVA Rescue (SAFER) Flight Test Project, %% Flight Test Article Prime Item Development Specification. %% NASA report JSC-25552A, July 1994. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% Several basic types are shared by all the SAFER theories. Various %% command types and null command constants are collected below. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% avionics_types: THEORY BEGIN pressure: TYPE = real temperature: TYPE = real voltage: TYPE = real angular_rate: TYPE = real linear_accel: TYPE = real axis_command: TYPE = {NEG, ZERO, POS} tran_axis: TYPE = {X, Y, Z} rot_axis: TYPE = {roll, pitch, yaw} tran_command: TYPE = [tran_axis -> axis_command] rot_command: TYPE = [rot_axis -> axis_command] rot_predicate: TYPE = [rot_axis -> bool] six_dof_command: TYPE = [# tran: tran_command, rot: rot_command #] null_tran_command: tran_command = (LAMBDA (a: tran_axis): ZERO) null_rot_command: rot_command = (LAMBDA (a: rot_axis): ZERO) null_six_dof: six_dof_command = (# tran := null_tran_command, rot := null_rot_command #) END avionics_types %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% The hand controller module (HCM) consists of a set of switches, %% a hand grip controller with integral pushbutton, and a set of %% crew displays. A six degree-of-freedom command is derived from %% four-axis hand grip inputs and the control mode switch position. %% It is assumed that switch debouncing is provided by a low-level %% hardware or software mechanism so that switch transitions in this %% model may be considered clean. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% hand_controller_module: THEORY BEGIN IMPORTING avionics_types power_test_switch: TYPE = {OFF, ON, TST} display_proceed_switch: TYPE = {PREV, CURR, NEXT} control_mode_switch: TYPE = {ROT, TRAN} AAH_control_button: TYPE = {button_up, button_down} HCM_switch_positions: TYPE = [# PWR: power_test_switch, DISP: display_proceed_switch, MODE: control_mode_switch, AAH: AAH_control_button #] %% The hand grip provides four axes for command input, which are %% multiplexed by the control mode switch into the required six axes. %% The four degrees of freedom on the controller are vertical, %% horizontal, transverse (along the shaft), and twist (about the shaft). hand_grip_position: TYPE = [# vert, horiz, trans, twist: axis_command #] grip_command(grip: hand_grip_position, mode: control_mode_switch): six_dof_command = (# tran := null_tran_command WITH [ X := horiz(grip), Y := IF mode = TRAN THEN trans(grip) ELSE ZERO ENDIF, Z := IF mode = TRAN THEN vert(grip) ELSE ZERO ENDIF], rot := null_rot_command WITH [ roll := IF mode = ROT THEN vert(grip) ELSE ZERO ENDIF, pitch := twist(grip), yaw := IF mode = ROT THEN trans(grip) ELSE ZERO ENDIF] #) %% The HCM display mechanism is centered around a 16-character LCD. char_display_index: TYPE = {n: nat | 1 <= n & n <= 16} CONTAINING 1 character_display: TYPE = [char_display_index -> character] blank_char_display: character_display = (LAMBDA (i: char_display_index): char(32)) HCM_display_set: TYPE = [# LCD: character_display, THR: bool, AAH: bool #] %% Multiline messages are stored in a buffer and viewed one line %% at a time. HCM_buffer_len: above[0] %% Any integer > 0 HCM_buffer_index: TYPE = {n: nat | 1 <= n & n <= HCM_buffer_len} CONTAINING 1 HCM_display_buffer: TYPE = [HCM_buffer_index -> character_display] blank_display_buffer: HCM_display_buffer = (LAMBDA (i: HCM_buffer_index): blank_char_display) %% The current pointer in the display state identifies which line to %% display, and the pointer can be moved up and down using the display %% proceed switch. HCM_display_state: TYPE = [# switch: display_proceed_switch, buffer: HCM_display_buffer, current: HCM_buffer_index #] next_disp_pointer(new_sw: display_proceed_switch, display: HCM_display_state): HCM_buffer_index = IF switch(display) = CURR AND new_sw /= CURR THEN IF new_sw = PREV THEN max(1, current(display) - 1) ELSE min(HCM_buffer_len, current(display) + 1) ENDIF ELSE current(display) ENDIF END hand_controller_module %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% The propulsion module provides a number of sensors and a set of %% actuators to control the 24 thrusters, which are grouped into %% four clusters or quadrants. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% propulsion_module: THEORY BEGIN IMPORTING avionics_types propulsion_sensors: TYPE = [# tank_press: pressure, tank_temp: temperature, reg_press: pressure, reg_temp: temperature, thruster_on: bool #] thruster_name: TYPE = {B1, B2, B3, B4, F1, F2, F3, F4, L1R, L1F, R2R, R2F, L3R, L3F, R4R, R4F, D1R, D1F, D2R, D2F, U3R, U3F, U4R, U4F} %% Thruster designators are triples of the form %% (thrust direction, cluster no., forward/rear location) %% Not all combinations of these values are possible so a dependent %% type is used to represent the constraints. thruster_direction: TYPE = {UP, DN, BK, FD, LT, RT} thruster_quadrant: TYPE = {n: nat | 1 <= n & n <= 4} CONTAINING 1 thruster_location: TYPE = {FW, RR} % forward, rear valid_quadrant(d: thruster_direction, q: thruster_quadrant): bool = COND d = UP -> q = 3 OR q = 4, d = DN -> q = 1 OR q = 2, d = LT -> q = 1 OR q = 3, d = RT -> q = 2 OR q = 4, ELSE -> true ENDCOND % Thrusters B1-B4 and F1-F4 are not normally written with a % forward/rear location tag, but they are supplied below to fit % the type declaration scheme. thruster_desig: TYPE = [ dir: thruster_direction, {quad: thruster_quadrant | valid_quadrant(dir, quad)}, {loc: thruster_location | (dir = BK => loc = FW) AND (dir = FD => loc = RR)} ] thruster_map(thruster: thruster_name): thruster_desig = TABLE thruster %--------------------% | B1 | (BK, 1, FW) || | B2 | (BK, 2, FW) || | B3 | (BK, 3, FW) || | B4 | (BK, 4, FW) || %--------------------% | F1 | (FD, 1, RR) || | F2 | (FD, 2, RR) || | F3 | (FD, 3, RR) || | F4 | (FD, 4, RR) || %--------------------% | L1R | (LT, 1, RR) || | L1F | (LT, 1, FW) || | R2R | (RT, 2, RR) || | R2F | (RT, 2, FW) || %--------------------% | L3R | (LT, 3, RR) || | L3F | (LT, 3, FW) || | R4R | (RT, 4, RR) || | R4F | (RT, 4, FW) || %--------------------% | D1R | (DN, 1, RR) || | D1F | (DN, 1, FW) || | D2R | (DN, 2, RR) || | D2F | (DN, 2, FW) || %--------------------% | U3R | (UP, 3, RR) || | U3F | (UP, 3, FW) || | U4R | (UP, 4, RR) || | U4F | (UP, 4, FW) || %--------------------% ENDTABLE END propulsion_module %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% Sensing for angular rotation rates and linear acceleration is %% provided by the inertial reference unit (IRU). %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% inertial_reference_unit: THEORY BEGIN IMPORTING avionics_types inertial_ref_sensors: TYPE = [# roll_rate: angular_rate, pitch_rate: angular_rate, yaw_rate: angular_rate, roll_temp: temperature, pitch_temp: temperature, yaw_temp: temperature, X_accel: linear_accel, Y_accel: linear_accel, Z_accel: linear_accel #] END inertial_reference_unit %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% An automatic attitude hold (AAH) capability may be invoked to %% maintain near-zero rotation rates. A pushbutton mounted on the %% hand grip engages AAH with a single button click, and disengages %% with a double click. Internal state information is maintained %% to observe the button pushing protocol, keep track of status for %% each axis, and implement the attitude hold control law. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% automatic_attitude_hold: THEORY BEGIN IMPORTING avionics_types, hand_controller_module, inertial_reference_unit, propulsion_module click_timeout: nat = 100 %% At most 0.5 second between button %% pushes for a double click. AAH_control_law_state: TYPE+ %% Unspecified, nonempty type AAH_engage_state: TYPE = {AAH_off, AAH_started, AAH_on, pressed_once, AAH_closing, pressed_twice} AAH_state: TYPE = [# active_axes: rot_predicate, ignore_HCM: rot_predicate, toggle: AAH_engage_state, timeout: nat, control_vars: AAH_control_law_state #] all_axes_off(active: rot_predicate): bool = (FORALL (a: rot_axis): NOT active(a)) %% On each frame, the sampled value of the AAH engage button is %% checked to determine whether AAH is engaging or disengaging. %% This function implements the AAH engagement state diagram. button_transition(state: AAH_engage_state, button: AAH_control_button, active: rot_predicate, clock: nat, timeout: nat): AAH_engage_state = TABLE state , button %---------------------------------% |[ button_down | button_up ]| %--------------------------------------------------% | AAH_off | AAH_started | AAH_off || | AAH_started | AAH_started | AAH_on || | AAH_on | pressed_once | state_A || | pressed_once | pressed_once | AAH_closing || | AAH_closing | pressed_twice | state_B || | pressed_twice | pressed_twice | AAH_off || %--------------------------------------------------% ENDTABLE WHERE state_A = IF all_axes_off(active) THEN AAH_off ELSE AAH_on ENDIF, state_B = IF all_axes_off(active) THEN AAH_off ELSIF clock > timeout THEN AAH_on ELSE AAH_closing ENDIF %% The control law used to implement attitude hold is represented by two %% functions that map sensor inputs and control law state into next state %% and output values. AAH_control_law(IRU_sensors: inertial_ref_sensors, prop_sensors: propulsion_sensors, AAH_state: AAH_state): AAH_control_law_state AAH_control_out(IRU_sensors: inertial_ref_sensors, prop_sensors: propulsion_sensors, AAH_state: AAH_state): rot_command initial_control_law_state: AAH_control_law_state %% AAH state information is updated in every frame. Key transitions in %% the engage-state diagram cause various state variables to be set. AAH_transition(IRU_sensors: inertial_ref_sensors, prop_sensors: propulsion_sensors, button_pos: AAH_control_button, HCM_cmd: six_dof_command, AAH_state: AAH_state, clock: nat): AAH_state = LET engage = button_transition(toggle(AAH_state), button_pos, active_axes(AAH_state), clock, timeout(AAH_state)), starting = (toggle(AAH_state) = AAH_off AND engage = AAH_started) IN (# active_axes := (LAMBDA (a: rot_axis): starting OR (engage /= AAH_off AND active_axes(AAH_state)(a) AND (rot(HCM_cmd)(a) = ZERO OR ignore_HCM(AAH_state)(a)))), ignore_HCM := (LAMBDA (a: rot_axis): IF starting THEN rot(HCM_cmd)(a) /= ZERO ELSE ignore_HCM(AAH_state)(a) ENDIF), toggle := engage, timeout := IF toggle(AAH_state) = AAH_on AND engage = pressed_once THEN clock + click_timeout ELSE timeout(AAH_state) ENDIF, control_vars := AAH_control_law(IRU_sensors, prop_sensors, AAH_state) #) END automatic_attitude_hold %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% Thruster selection logic is formalized in the following theory. %% Hand controller and AAH commands are merged together in accordance %% with the various priority rules, yielding a six degree-of-freedom %% command. Thruster selection tables are consulted to convert the %% translation and rotation components to individual actuator %% commands for opening suitable thruster valves. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% thruster_selection: THEORY BEGIN IMPORTING avionics_types, propulsion_module, automatic_attitude_hold %% Actuator commands are modeled as a list of thrusters to be fired. thruster_list: TYPE = list[thruster_name] actuator_commands: TYPE = thruster_list null_actuation: actuator_commands = (: :) %% Empty list %% Utility functions needed later. rot_cmds_present(cmd: rot_command): bool = (EXISTS (a: rot_axis): cmd(a) /= ZERO) %% At most one translation is allowed, in priority order X, Y, Z. prioritized_tran_cmd(tran: tran_command): tran_command = IF tran(X) /= ZERO THEN null_tran_command WITH [X := tran(X)] ELSIF tran(Y) /= ZERO THEN null_tran_command WITH [Y := tran(Y)] ELSIF tran(Z) /= ZERO THEN null_tran_command WITH [Z := tran(Z)] ELSE null_tran_command ENDIF %% Hand grip rotation commands take precedence over AAH commands %% unless inhibited at the start of AAH. combined_rot_cmds(HCM_rot: rot_command, AAH: rot_command, ignore_HCM: rot_predicate): rot_command = (LAMBDA (a: rot_axis): IF HCM_rot(a) = ZERO OR ignore_HCM(a) THEN AAH(a) ELSE HCM_rot(a) ENDIF) %% Hand grip rotations suppress translations but AAH rotations do not. integrated_commands(HCM: six_dof_command, AAH: rot_command, state: AAH_state): six_dof_command = IF all_axes_off(active_axes(state)) THEN IF rot_cmds_present(rot(HCM)) THEN (# tran := null_tran_command, rot := rot(HCM) #) ELSE (# tran := prioritized_tran_cmd(tran(HCM)), rot := null_rot_command #) ENDIF ELSE IF rot_cmds_present(rot(HCM)) THEN (# tran := null_tran_command, rot := combined_rot_cmds(rot(HCM), AAH, ignore_HCM(state)) #) ELSE (# tran := prioritized_tran_cmd(tran(HCM)), rot := AAH #) ENDIF ENDIF %% Selection of back and forward thrusters results in a pair of %% thruster lists, the first of which gives mandatory thrusters %% and the second gives optional thrusters. (Mandatory means %% always selected while optional means conditionally selected.) %% This function represents the selection table for X, pitch, %% and yaw commands. thruster_list_pair: TYPE = [thruster_list, thruster_list] BF_thrusters(A, B, C: axis_command): thruster_list_pair = TABLE A | NEG | TABLE B | NEG | TABLE C %--------------------------------------% | NEG | ((: B4 :), (: B2, B3 :)) || | ZERO | ((: B3, B4 :), (: :)) || | POS | ((: B3 :), (: B1, B4 :)) || %--------------------------------------% ENDTABLE || | ZERO | TABLE C %--------------------------------------% | NEG | ((: B2, B4 :), (: :)) || | ZERO | ((: B1, B4 :), (: B2, B3 :)) || | POS | ((: B1, B3 :), (: :)) || %--------------------------------------% ENDTABLE || | POS | TABLE C %--------------------------------------% | NEG | ((: B2 :), (: B1, B4 :)) || | ZERO | ((: B1, B2 :), (: :)) || | POS | ((: B1 :), (: B2, B3 :)) || %--------------------------------------% ENDTABLE || ENDTABLE || | ZERO | TABLE B | NEG | TABLE C %--------------------------------------% | NEG | ((: B4, F1 :), (: :)) || | ZERO | ((: B4, F2 :), (: :)) || | POS | ((: B3, F2 :), (: :)) || %--------------------------------------% ENDTABLE || | ZERO | TABLE C %--------------------------------------% | NEG | ((: B2, F1 :), (: :)) || | ZERO | ((: :), (: :)) || | POS | ((: B3, F4 :), (: :)) || %--------------------------------------% ENDTABLE || | POS | TABLE C %--------------------------------------% | NEG | ((: B2, F3 :), (: :)) || | ZERO | ((: B1, F3 :), (: :)) || | POS | ((: B1, F4 :), (: :)) || %--------------------------------------% ENDTABLE || ENDTABLE || | POS | TABLE B | NEG | TABLE C %--------------------------------------% | NEG | ((: F1 :), (: F2, F3 :)) || | ZERO | ((: F1, F2 :), (: :)) || | POS | ((: F2 :), (: F1, F4 :)) || %--------------------------------------% ENDTABLE || | ZERO | TABLE C %--------------------------------------% | NEG | ((: F1, F3 :), (: :)) || | ZERO | ((: F2, F3 :), (: F1, F4 :)) || | POS | ((: F2, F4 :), (: :)) || %--------------------------------------% ENDTABLE || | POS | TABLE C %--------------------------------------% | NEG | ((: F3 :), (: F1, F4 :)) || | ZERO | ((: F3, F4 :), (: :)) || | POS | ((: F4 :), (: F2, F3 :)) || %--------------------------------------% ENDTABLE || ENDTABLE || ENDTABLE %% Selection of left, right, up, and down thrusters resulting from %% Y, Z, and roll commands. LRUD_thrusters(A, B, C: axis_command): thruster_list_pair = TABLE A | NEG | TABLE B | NEG | TABLE C %------------------------------------------% | NEG | ((: :), (: :)) || | ZERO | ((: :), (: :)) || | POS | ((: :), (: :)) || %------------------------------------------% ENDTABLE || | ZERO | TABLE C %------------------------------------------% | NEG | ((: L1R :), (: L1F, L3F :)) || | ZERO | ((: L1R, L3R :), (: L1F, L3F :)) || | POS | ((: L3R :), (: L1F, L3F :)) || %------------------------------------------% ENDTABLE || | POS | TABLE C %------------------------------------------% | NEG | ((: :), (: :)) || | ZERO | ((: :), (: :)) || | POS | ((: :), (: :)) || %------------------------------------------% ENDTABLE || ENDTABLE || | ZERO | TABLE B | NEG | TABLE C %------------------------------------------% | NEG | ((: U3R :), (: U3F, U4F :)) || | ZERO | ((: U3R, U4R :), (: U3F, U4F :)) || | POS | ((: U4R :), (: U3F, U4F :)) || %------------------------------------------% ENDTABLE || | ZERO | TABLE C %------------------------------------------% | NEG | ((: L1R, R4R :), (: :)) || | ZERO | ((: :), (: :)) || | POS | ((: R2R, L3R :), (: :)) || %------------------------------------------% ENDTABLE || | POS | TABLE C %------------------------------------------% | NEG | ((: D2R :), (: D1F, D2F :)) || | ZERO | ((: D1R, D2R :), (: D1F, D2F :)) || | POS | ((: D1R :), (: D1F, D2F :)) || %------------------------------------------% ENDTABLE || ENDTABLE || | POS | TABLE B | NEG | TABLE C %------------------------------------------% | NEG | ((: :), (: :)) || | ZERO | ((: :), (: :)) || | POS | ((: :), (: :)) || %------------------------------------------% ENDTABLE || | ZERO | TABLE C %------------------------------------------% | NEG | ((: R4R :), (: R2F, R4F :)) || | ZERO | ((: R2R, R4R :), (: R2F, R4F :)) || | POS | ((: R2R :), (: R2F, R4F :)) || %------------------------------------------% ENDTABLE || | POS | TABLE C %------------------------------------------% | NEG | ((: :), (: :)) || | ZERO | ((: :), (: :)) || | POS | ((: :), (: :)) || %------------------------------------------% ENDTABLE || ENDTABLE || ENDTABLE %% An integrated six degree-of-freedom command is mapped into a vector %% of actuator commands. Selection tables provide lists of thrusters %% and both mandatory and optional thrusters are included as appropriate. selected_thrusters(cmd: six_dof_command): thruster_list = LET (BF_mandatory, BF_optional) = BF_thrusters(tran(cmd)(X), rot(cmd)(pitch), rot(cmd)(yaw)), (LRUD_mandatory, LRUD_optional) = LRUD_thrusters(tran(cmd)(Y), tran(cmd)(Z), rot(cmd)(roll)), BF_thr = append(IF rot(cmd)(roll) = ZERO THEN BF_optional ELSE (: :) ENDIF, BF_mandatory), LRUD_thr = append(IF rot(cmd)(pitch) = ZERO AND rot(cmd)(yaw) = ZERO THEN LRUD_optional ELSE (: :) ENDIF, LRUD_mandatory) IN append(BF_thr, LRUD_thr) selected_actuators(HCM: six_dof_command, AAH: rot_command, state: AAH_state): actuator_commands = selected_thrusters(integrated_commands(HCM, AAH, state)) END thruster_selection %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% Several sensors are provided by the power supply to support %% the fault monitoring functions. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% power_supply: THEORY BEGIN IMPORTING avionics_types power_supply_sensors: TYPE = [# elect_batt: voltage, valve_batt: voltage, batt_temp: temperature #] END power_supply %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% A data recorder module is provided to record SAFER performance %% data for later analysis. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% data_recorder: THEORY BEGIN IMPORTING avionics_types, propulsion_module, inertial_reference_unit, thruster_selection, power_supply, automatic_attitude_hold data_recorder_packet: TYPE+ data_packet(prop_sensors: propulsion_sensors, IRU_sensors: inertial_ref_sensors, power_sensors: power_supply_sensors, AAH_state: AAH_state, thrusters: actuator_commands): data_recorder_packet END data_recorder %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% Continuous fault monitoring and consumables monitoring is %% provided by the self-test function. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% self_test: THEORY BEGIN IMPORTING avionics_types, propulsion_module, inertial_reference_unit, power_supply, automatic_attitude_hold self_test_state: TYPE+ initial_self_test_state: self_test_state %% The monitoring function is provided by the following. SAFER_monitoring(prop_sensors: propulsion_sensors, IRU_sensors: inertial_ref_sensors, power_sensors: power_supply_sensors, self_test: self_test_state): self_test_state END self_test %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% Data from the various SAFER modules is collected for crew display %% through the HCM character display. %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% HCM_display: THEORY BEGIN IMPORTING avionics_types, hand_controller_module, self_test %% The HCM display buffer is constructed and updated by the following. display_buffer(self_test: self_test_state, HCM_display: HCM_display_buffer): HCM_display_buffer initial_display_buffer: HCM_display_buffer END HCM_display %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% The top level state machine model of the controller is presented %% in the following theory. A transition function describes the %% effects of the controller's actions during a single frame. A %% 5 msec frame period is assumed (200 Hz sampling rate). %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% avionics_model: THEORY BEGIN IMPORTING avionics_types, hand_controller_module, propulsion_module, thruster_selection, inertial_reference_unit, automatic_attitude_hold, data_recorder, power_supply, self_test, HCM_display %% Controller inputs from SAFER modules and components. avionics_inputs: TYPE = [# HCM_switches: HCM_switch_positions, grip_command: hand_grip_position, prop_sensors: propulsion_sensors, IRU_sensors: inertial_ref_sensors, power_sensors: power_supply_sensors #] %% Controller outputs to SAFER modules and components. avionics_outputs: TYPE = [# HCM_displays: HCM_display_set, prop_actuators: actuator_commands, data_recorder: data_recorder_packet #] %% Internal state variables maintained by the controller. avionics_state: TYPE = [# msg_display: HCM_display_state, AAH_state: AAH_state, clock: nat, self_test: self_test_state #] avionics_result: TYPE = [# output: avionics_outputs, state: avionics_state #] %% The top level state machine transition function represents one %% frame of controller operation (once around the main control loop). SAFER_control (avionics_inputs: avionics_inputs, avionics_state: avionics_state): avionics_result = LET switches = HCM_switches(avionics_inputs), raw_grip = grip_command(avionics_inputs), prop_sensors = prop_sensors(avionics_inputs), IRU_sensors = IRU_sensors(avionics_inputs), power_sensors = power_sensors(avionics_inputs), AAH_state = AAH_state(avionics_state), AAH_active = NOT all_axes_off(active_axes(AAH_state)), display = msg_display(avionics_state), clock = clock(avionics_state), self_test = self_test(avionics_state), grip_cmd = grip_command(raw_grip, MODE(switches)), AAH_cmd = AAH_control_out(IRU_sensors, prop_sensors, AAH_state), thrusters = selected_actuators(grip_cmd, AAH_cmd, AAH_state), monitoring = SAFER_monitoring(prop_sensors, IRU_sensors, power_sensors, self_test), disp_window = buffer(display)(current(display)), disp_buffer = display_buffer(monitoring, buffer(display)), disp_pointer = next_disp_pointer(DISP(switches), display) IN (# output := (# HCM_displays := (# LCD := disp_window, THR := thruster_on(prop_sensors), AAH := AAH_active #), prop_actuators := thrusters, data_recorder := data_packet(prop_sensors, IRU_sensors, power_sensors, AAH_state, thrusters) #), state := (# msg_display := (# switch := DISP(switches), buffer := disp_buffer, current := disp_pointer #), AAH_state := AAH_transition(IRU_sensors, prop_sensors, AAH(switches), grip_cmd, AAH_state, clock), clock := 1 + clock, self_test := monitoring #) #) %% The controller is assumed to be powered up into the following %% initial state. initial_avionics_state: avionics_state = (# msg_display := (# switch := CURR, buffer := initial_display_buffer, current := 1 #), AAH_state := (# active_axes := (LAMBDA (a: rot_axis): false), ignore_HCM := (LAMBDA (a: rot_axis): false), toggle := AAH_off, timeout := 0, control_vars := initial_control_law_state #), clock := 0, self_test := initial_self_test_state #) END avionics_model