Permalink
Switch branches/tags
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
442 lines (389 sloc) 14.2 KB
--
-- CSP Model of the smart watch embedded application
--
-- Author: J. German Rivera
--
--
-- Event Alphabets
--
datatype ALPHABET =
initialize_serial_console |
initialize_dma_engine |
initialize_watch |
initialize_low_power |
initialize_lcd_display |
initialize_lcd_display_spi_interface |
initialize_accelerometer |
initialize_accelerometer_i2c_interface |
initialize_heart_rate_monitor |
initialize_heart_rate_monitor_i2c_interface |
initialize_barometric_pressure_sensor |
initialize_barometric_pressure_sensor_i2c_interface |
initialize_bluetooth |
display_console_greeting |
display_lcd_display_greeting |
parse_console_command |
schedule_deep_sleep |
start_dma_transfer_to_display |
start_i2c_byte_transfer_for_accelerometer |
turn_off_lcd_display |
turn_on_lcd_display |
refresh_current_altitude |
refresh_current_heart_rate |
refresh_current_temperature |
refresh_current_battery_charge |
refresh_wall_time |
refresh_whole_lcd_display |
start_heart_rate_monitor |
stop_heart_rate_monitor |
activate_barometric_pressure_sensor |
deactivate_barometric_pressure_sensor |
low_power_sleep_wakeup_callback |
realtime_clock_alarm_callback |
realtime_clock_seconds_callback |
read_heart_rate |
read_temperature |
read_altitude |
i2c_read |
transmit_byte_on_console_uart |
low_power_sleep_timeout |
low_power_sleep_wakeup |
heart_rate_changed |
altitude_changed |
temperature_changed |
wall_time_changed |
battery_charge_changed |
tapping_detected |
double_tapping_detected
APP_EVENTS_ALPHABET = { low_power_sleep_timeout,
low_power_sleep_wakeup,
heart_rate_changed,
altitude_changed,
temperature_changed,
wall_time_changed,
battery_charge_changed,
tapping_detected,
double_tapping_detected }
APP_ACTIONS_ALPHABET = {
initialize_serial_console,
initialize_dma_engine,
initialize_watch,
initialize_low_power,
initialize_lcd_display,
initialize_lcd_display_spi_interface,
initialize_accelerometer,
initialize_accelerometer_i2c_interface,
initialize_heart_rate_monitor,
initialize_heart_rate_monitor_i2c_interface,
initialize_barometric_pressure_sensor,
initialize_barometric_pressure_sensor_i2c_interface,
initialize_bluetooth,
display_console_greeting,
display_lcd_display_greeting,
parse_console_command,
schedule_deep_sleep,
start_dma_transfer_to_display,
start_i2c_byte_transfer_for_accelerometer,
turn_off_lcd_display,
turn_on_lcd_display,
refresh_current_altitude,
refresh_current_heart_rate,
refresh_current_temperature,
refresh_current_battery_charge,
refresh_wall_time,
refresh_whole_lcd_display,
start_heart_rate_monitor,
stop_heart_rate_monitor,
activate_barometric_pressure_sensor,
deactivate_barometric_pressure_sensor,
low_power_sleep_wakeup_callback,
realtime_clock_alarm_callback,
realtime_clock_seconds_callback,
read_heart_rate,
read_temperature,
read_altitude,
i2c_read,
transmit_byte_on_console_uart }
--
-- Event Channels
--
channel watch_task_susp_obj
channel tapping_detection_task_susp_obj
channel serial_console_output_task_susp_obj
channel tapping_detected_susp_obj
channel accelerometer_tapping_detected_isr_susp_obj
channel display_dma_transfer_completed_isr_susp_obj
channel serial_console_uart_byte_received_isr_susp_obj
channel bluetooth_uart_byte_received_isr_susp_obj
channel heart_rate_monitor_proximity_sensed_isr_susp_obj
channel heart_rate_monitor_sample_ready_isr_susp_obj
channel heart_rate_monitor_task_susp_obj
channel altitude_changed_isr_susp_obj
channel altitude_sensor_task_susp_obj
channel temperature_changed_isr_susp_obj
channel temperature_sensor_task_susp_obj
channel altitude_reading_prot_entry
channel temperature_reading_prot_entry
channel accelerometer_tapping_detected_interrupt
channel display_dma_transfer_completed_interrupt
channel accelerometer_i2c_byte_transfer_completed_interrupt
channel serial_console_uart_byte_received_interrupt
channel bluetooth_uart_byte_received_interrupt
channel low_leakage_stop_wakeup_interrupt
channel heart_rate_monitor_proximity_sensed_interrupt
channel heart_rate_monitor_sample_ready_interrupt
channel altitude_changed_interrupt
channel temperature_changed_interrupt
channel realtime_clock_alarm_interrupt
channel realtime_clock_seconds_interrupt
channel event : APP_EVENTS_ALPHABET
channel action : APP_ACTIONS_ALPHABET
SUSPENSION_OBJECTS = {| watch_task_susp_obj,
tapping_detection_task_susp_obj,
serial_console_output_task_susp_obj,
accelerometer_tapping_detected_isr_susp_obj,
display_dma_transfer_completed_isr_susp_obj,
serial_console_uart_byte_received_isr_susp_obj,
bluetooth_uart_byte_received_isr_susp_obj,
heart_rate_monitor_proximity_sensed_isr_susp_obj,
heart_rate_monitor_sample_ready_isr_susp_obj,
heart_rate_monitor_task_susp_obj,
altitude_changed_isr_susp_obj,
altitude_sensor_task_susp_obj,
temperature_changed_isr_susp_obj,
temperature_sensor_task_susp_obj |}
PROTECTED_ENTRIES = {| altitude_reading_prot_entry,
temperature_reading_prot_entry |}
INTERRUPTS = {| accelerometer_tapping_detected_interrupt,
accelerometer_i2c_byte_transfer_completed_interrupt,
display_dma_transfer_completed_interrupt,
serial_console_uart_byte_received_interrupt,
bluetooth_uart_byte_received_interrupt,
low_leakage_stop_wakeup_interrupt,
realtime_clock_alarm_interrupt,
realtime_clock_seconds_interrupt,
heart_rate_monitor_proximity_sensed_interrupt,
heart_rate_monitor_sample_ready_interrupt,
altitude_changed_interrupt,
temperature_changed_interrupt,
realtime_clock_alarm_interrupt,
realtime_clock_seconds_interrupt |}
--
-- CSP Processes
--
SMART_WATCH_APP =
((MAIN_TASK
[| {| serial_console_output_task_susp_obj, watch_task_susp_obj |} |]
(SERIAL_CONSOLE_OUTPUT_TASK |||
WATCH_APP_TASKS))
[| SUSPENSION_OBJECTS |]
INTERRUPT_HANDLERS)
assert SMART_WATCH_APP :[deadlock free]
assert SMART_WATCH_APP :[divergence free]
WATCH_APP_TASKS =
WATCH_TASK
[| {| event |} |]
(TAPPING_DETECTION |||
HEART_RATE_MONITOR_TASK |||
TEMPERATURE_SENSOR_TASK |||
ALTITUDE_SENSOR_TASK)
TAPPING_DETECTION =
TAPPING_DETECTION_TASK [| tapping_detected_susp_obj |]
(ACCELEROMETER_TAPPING_DETECTED_INT_TASK
[| accelerometer_tapping_detected_isr_susp_obj |]
ACCELEROMETER_TAPPING_DETECTED_ISR)
HEART_RATE_MONITOR =
HEART_RATE_MONITOR_TASK [| |]
INTERRUPT_HANDLERS =
SERIAL_CONSOLE_UART_BYTE_RECEIVED_ISR |||
BLUETOOTH_UART_BYTE_RECEIVED_ISR |||
LOW_POWER_SLEEP_WAKEUP_ISR |||
(HEART_RATE_MONITOR_PROXIMITY_SENSED_ISR
[| heart_rate_monitor_proximity_sensed_isr_susp_obj |]
HEART_RATE_MONITOR_PROXIMITY_SENSED_INT_TASK) |||
HEART_RATE_MONITOR_SAMPLE_READY_ISR |||
(ALTITUDE_CHANGED_ISR [| altitude_changed_isr_susp_obj |]
ALTITUDE_CHANGED_INT_TASK) |||
(TEMPERATURE_CHANGED_ISR [| temperature_changed_isr_susp_obj |]
TEMPERATURE_CHANGED_INT_TASK) |||
REALTIME_CLOCK_ALARM_ISR |||
REALTIME_CLOCK_SECONDS_ISR
MAIN_TASK = action!initialize_serial_console ->
serial_console_output_task_susp_obj! ->
action!display_console_greeting ->
action!initialize_dma_engine ->
action!initialize_bluetooth ->
action!initialize_watch ->
action!initialize_low_power ->
action!initialize_accelerometer ->
action!initialize_accelerometer_i2c_interface ->
action!initialize_heart_rate_monitor ->
action!initialize_heart_rate_monitor_i2c_interface ->
action!start_heart_rate_monitor ->
action!initialize_barometric_pressure_sensor ->
action!initialize_barometric_pressure_sensor_i2c_interface ->
action!activate_barometric_pressure_sensor ->
watch_task_susp_obj.set_true ->
READ_COMMAND_LOOP
SERIAL_CONSOLE_OUTPUT_TASK =
serial_console_output_task_susp_obj.suspend_until_true ->
SEND_CONSOLE_OUTPUT_LOOP
SEND_CONSOLE_OUTPUT_LOOP =
action!transmit_byte_on_console_uart -> SEND_CONSOLE_OUTPUT_LOOP
READ_COMMAND_LOOP =
serial_console_uart_byte_received_isr_susp_obj.suspend_until_true ->
action!parse_console_command -> READ_COMMAND_LOOP
WATCH_TASK =
watch_task_susp_obj.suspend_until_true ->
action!initialize_lcd_display ->
action!initialize_lcd_display_spi_interface ->
action!display_lcd_display_greeting ->
heart_rate_monitor_task_susp_obj!set_true ->
altitude_sensor_task_susp_obj!set_true ->
temperature_sensor_task_susp_obj!set_true ->
action!refresh_whole_lcd_display ->
display_dma_transfer_completed_isr_susp_obj ->
WATCH_STATE_MACHINE
WATCH_STATE_MACHINE = AWAKE_WATCH_MODE
assert WATCH_STATE_MACHINE :[deterministic]
AWAKE_WATCH_MODE =
event.wall_time_changed ->
action!refresh_wall_time -> AWAKE_WATCH_MODE
[]
event.low_power_sleep_timeout ->
action!turn_off_lcd_display ->
action!stop_heart_rate_monitor ->
heart_rate_monitor_proximity_sensed_interrupt.disable ->
action!deactivate_barometric_pressure_sensor ->
temperature_changed_interrupt.disable ->
altitude_changed_interrupt.disable ->
action!schedule_deep_sleep ->
watch_task_susp_obj.suspend_until_true -> ASLEEP_WATCH_MODE
[]
event.heart_rate_changed ->
action!refresh_current_heart_rate -> AWAKE_WATCH_MODE
[]
event.temperature_changed -> action!refresh_current_temperature -> AWAKE_WATCH_MODE
[]
event.altitude_changed -> action!refresh_current_altitude -> AWAKE_WATCH_MODE
[]
event.battery_charge_changed -> action!refresh_current_battery_charge -> AWAKE_WATCH_MODE
[]
event.tapping_detected -> AWAKE_WATCH_MODE
[]
event.double_tapping_detected -> AWAKE_WATCH_MODE
[]
watch_task_susp_obj.suspend_until_true -> AWAKE_WATCH_MODE
ASLEEP_WATCH_MODE =
event.low_power_sleep_wakeup ->
action!start_heart_rate_monitor ->
action!activate_barometric_pressure_sensor ->
action!turn_on_lcd_display ->
action!refresh_whole_lcd_display ->
display_dma_transfer_completed_isr_susp_obj ->
AWAKE_WATCH_MODE
[]
watch_task_susp_obj.suspend_until_true -> ASLEEP_WATCH_MODE
TAPPING_DETECTION_TASK =
accelerometer_tapping_detected_isr_susp_obj ->
(event!tapping_detected -> TAPPING_DETECTION_TASK
|~|
event!double_tapping_detected -> TAPPING_DETECTION_TASK)
HEART_RATE_MONITOR_TASK =
heart_rate_monitor_task_susp_obj -> HEART_RATE_MONITOR_TASK_STARTED
HEART_RATE_MONITOR_TASK_STARTED =
action!read_heart_rate ->
heart_rate_monitor_sample_ready_isr_susp_obj ->
action!i2c_read ->
(event!heart_rate_changed ->
watch_task_susp_obj! -> HEART_RATE_MONITOR_TASK_STARTED
|~|
HEART_RATE_MONITOR_TASK_STARTED)
ALTITUDE_SENSOR_TASK =
altitude_sensor_task_susp_obj -> ALTITUDE_SENSOR_TASK_STARTED
ALTITUDE_SENSOR_TASK_STARTED =
action!read_altitude ->
altitude_reading_prot_entry ->
(event!altitude_changed ->
watch_task_susp_obj! -> ALTITUDE_SENSOR_TASK_STARTED
|~|
ALTITUDE_SENSOR_TASK_STARTED)
TEMPERATURE_SENSOR_TASK =
temperature_sensor_task_susp_obj -> TEMPERATURE_SENSOR_TASK_STARTED
TEMPERATURE_SENSOR_TASK_STARTED =
action!read_temperature ->
temperature_reading_prot_entry ->
(event!temperature_changed ->
watch_task_susp_obj! -> TEMPERATURE_SENSOR_TASK_STARTED
|~|
TEMPERATURE_SENSOR_TASK_STARTED)
ACCELEROMETER_TAPPING_DETECTED_ISR =
accelerometer_tapping_detected_interrupt ->
accelerometer_tapping_detected_isr_susp_obj! ->
ACCELEROMETER_TAPPING_DETECTED_ISR
ACCELEROMETER_TAPPING_DETECTED_INT_TASK =
accelerometer_tapping_detected_isr_susp_obj ->
action!i2c_read ->
tapping_detected_susp_obj! ->
ACCELEROMETER_TAPPING_DETECTED_INT_TASK
SERIAL_CONSOLE_UART_BYTE_RECEIVED_ISR =
serial_console_uart_byte_received_interrupt ->
serial_console_uart_byte_received_isr_susp_obj! ->
SERIAL_CONSOLE_UART_BYTE_RECEIVED_ISR
BLUETOOTH_UART_BYTE_RECEIVED_ISR =
bluetooth_uart_byte_received_interrupt ->
bluetooth_uart_byte_received_isr_susp_obj! ->
BLUETOOTH_UART_BYTE_RECEIVED_ISR
HEART_RATE_MONITOR_PROXIMITY_SENSED_ISR =
heart_rate_monitor_proximity_sensed_interrupt ->
heart_rate_monitor_proximity_sensed_isr_susp_obj! ->
HEART_RATE_MONITOR_PROXIMITY_SENSED_ISR
HEART_RATE_MONITOR_PROXIMITY_SENSED_INT_TASK =
heart_rate_monitor_proximity_sensed_isr_susp_obj ->
heart_rate_monitor_sample_ready_interrupt_enable! ->
HEART_RATE_MONITOR_PROXIMITY_SENSED_INT_TASK
HEART_RATE_MONITOR_SAMPLE_READY_ISR =
heart_rate_monitor_sample_ready_interrupt_enable ->
HEART_RATE_MONITOR_SAMPLE_READY_ISR_ENABLED
HEART_RATE_MONITOR_SAMPLE_READY_ISR_ENABLED =
heart_rate_monitor_sample_ready_interrupt ->
heart_rate_monitor_sample_ready_isr_susp_obj! ->
HEART_RATE_MONITOR_SAMPLE_READY_ISR_ENABLED
[]
heart_rate_monitor_sample_ready_interrupt_disable ->
HEART_RATE_MONITOR_SAMPLE_READY_ISR
ALTITUDE_CHANGED_ISR =
altitude_changed_interrupt -> altitude_changed_isr_susp_obj! ->
ALTITUDE_CHANGED_ISR
ALTITUDE_CHANGED_INT_TASK =
altitude_changed_isr_susp_obj ->
action!i2c_read ->
altitude_reading_prot_entry! ->
ALTITUDE_CHANGED_INT_TASK
TEMPERATURE_CHANGED_ISR =
temperature_changed_interrupt ->
temperature_changed_isr_susp_obj! ->
TEMPERATURE_CHANGED_ISR
TEMPERATURE_CHANGED_INT_TASK =
temperature_changed_isr_susp_obj ->
action!i2c_read ->
temperature_reading_prot_entry! ->
TEMPERATURE_CHANGED_INT_TASK
REALTIME_CLOCK_ALARM_ISR =
realtime_clock_alarm_interrupt.fired ->
action!realtime_clock_alarm_callback ->
event!low_power_sleep_timeout ->
watch_task_susp_obj!set_true ->
REALTIME_CLOCK_ALARM_ISR
REALTIME_CLOCK_SECONDS_ISR =
realtime_clock_seconds_interrupt.fired ->
action!realtime_clock_seconds_callback ->
event!wall_time_changed ->
watch_task_susp_obj!set_true ->
REALTIME_CLOCK_SECONDS_ISR
LOW_POWER_SLEEP_WAKEUP_ISR =
low_leakage_stop_wakeup_interrupt.fired ->
action!low_power_sleep_wakeup_callback ->
event!low_power_sleep_wakeup ->
watch_task_susp_obj!set_true ->
LOW_POWER_SLEEP_WAKEUP_ISR