Banking system
(legacy PauWare ver. 1.3)
Preamble

Banking system is a software case study, which is implemented in State Chart XML (SCXML) and PauWare. PauWare is a Java engine for executing Harel's Statecharts in general.

Goal

This case study is a banking system. The Requirements Definition Doc. is ☛ (PDF, Chap. 6, in French).

Resources
Implementation in PauWare (ver. 1.3) and JavaFX
Specification (Card reader, Cash dispenser…)
Specification (Transaction)
Specification (ATM) as full-size SVG image
ATM Working Transaction_in_progress Out_of_order entry/ ATM.display_out_of_order End entry/ Card_reader.card_to_be_ejected entry/ ATM.display_take_card exit/ Transaction_manager.to_be_recorded Second_delaying exit/ ATM.to_be_killed(Statechart) exit/ ATM.to_be_killed(Statechart) Suspicious_end entry/ Card_reader.card_to_be_put_down exit/ Transaction_manager.to_be_recorded Transaction_verification entry/ ATM.to_be_set(Statechart,Long) entry/ ATM.display_transaction_starts_ exit/ ATM.to_be_killed(Statechart) Password_request entry/ ATM.to_be_set(Statechart,Long) entry/ ATM.display_enter_password exit/ ATM.to_be_killed(Statechart) Printing Start entry/ ATM.display_insert_card Brief_end entry/ Card_reader.card_to_be_ejected entry/ ATM.display_take_card First_delaying entry/ ATM.to_be_set(Statechart,Long) exit/ ATM.to_be_killed(Statechart) Third_delaying entry/ ATM.to_be_set(Statechart,Long) exit/ ATM.to_be_killed(Statechart) Deposit_in_progress Withdrawal_in_progress Operation_verification entry/ ATM.to_be_set(Statechart,Long) entry/ ATM.display_operation_starts_ exit/ ATM.to_be_killed(Statechart) Transaction_end_choice entry/ ATM.display_choose_continuation_or_termination Account_choice entry/ ATM.display_choose_account Operation_kind_choice entry/ ATM.display_choose_operation_kind Amount_choice entry/ ATM.to_be_set(Statechart,Long) entry/ ATM.display_choose_amount exit/ ATM.to_be_killed(Statechart) Amount_verification time_out card_unreadable/ATM.display_card_unreadable card_put_down/ATM.display_card_put_down card_removed transaction_empty[ATM.breakdown_equal_to_false] transaction_not_empty[ATM.breakdown_equal_to_false]/Receipt_printer.to_be_printed(Transaction_manager) card_read/ATM.set_attempt_(Byte) password_entered[ATM.password_equal_to_authorisation_password(String)]/^Consortium.start_of(String,Object,Timestamp) card_put_down/ATM.display_card_put_down time_out[ATM.context_equal_to_Password_request_and_attempt_equal_to_2(Statechart)] password_entered[ATM.password_not_equal_to_authorisation_password(String)]/ATM.display_invalid_password;ATM.to_be_set(Statechart,Long) time_out[ATM.context_equal_to_Password_request_and_attempt_equal_to_1(Statechart)]/ATM.set_attempt_(Byte) response_to_START_OF_not_ok/ATM.display_transaction_error(String);Transaction_manager.error(String);ATM.to_be_set(Statechart,Long) card_removed/^Transaction_manager.empty_ time_out time_out[ATM.context_equal_to_Transaction_verification(Statechart)] time_out/Consortium.end_of(String,Object) card_put_down[ATM.breakdown_equal_to_false]/ATM.display_card_put_down operation_kind_chosen[ATM.operation_is_not_Query]/ATM.set_amount_choice_try_to(Byte);ATM.set_again_to(Boolean) amount_chosen[ATM.operation_is_Withdrawal]/^Cash_dispenser.enough_(Integer) amount_chosen[ATM.operation_is_Deposit][ATM.operation_is_Transfer]/ATM.set_transfer_end(Boolean) operation_kind_chosen[ATM.operation_is_Query] enough_cash[ATM.amount_less_or_equal_to_authorisation_withdrawal_weekly_limit] continuation response_to_TO_BE_PROCESSED_ok[ATM.operation_is_Withdrawal]/Transaction_manager.to_be_added(Operation);^Cash_dispenser.to_be_dispensed(Integer) response_to_TO_BE_PROCESSED_ok[ATM.operation_is_Deposit]/^Deposit_drawer.to_be_deposited;Transaction_manager.to_be_added(Operation) time_out[ATM.amount_choice_try_not_equal_to_2] enough_cash[ATM.amount_greater_than_authorisation_withdrawal_weekly_limit]/ATM.display_operation_error(String);ATM.set_amount_choice_try_to(Byte);ATM.set_again_to(Boolean) not_enough_cash/ATM.display_operation_error(String);ATM.set_amount_choice_try_to(Byte);ATM.set_again_to(Boolean) response_to_TO_BE_PROCESSED_not_ok/ATM.display_operation_error(String) response_to_TO_BE_PROCESSED_ok[ATM.operation_is_Query_or_Transfer]/Transaction_manager.to_be_added(Operation);ATM.display_account withdrawal_done/ATM.display_account time_out[ATM.amount_choice_try_equal_to_2] deposit_done/ATM.display_account deposit_drawer_breakdown/ATM.set_breakdown(Boolean);Consortium.to_be_canceled(String,Object,Object) time_out/Consortium.end_of(String,Object) termination/Consortium.end_of(String,Object) time_out/Consortium.end_of(String,Object);Consortium.to_be_canceled(String,Object,Object) cash_dispenser_breakdown/ATM.set_breakdown(Boolean);Consortium.to_be_canceled(String,Object,Object) response_to_START_OF_ok abort/Consortium.end_of(String,Object) card_reader_breakdown receipt_printer_breakdown card_put_down[ATM.breakdown_equal_to_true] transaction_empty[ATM.breakdown_equal_to_true] transaction_not_empty[ATM.breakdown_equal_to_true]/Receipt_printer.to_be_printed(Transaction_manager) repairing/ATM.set_breakdown(Boolean);Card_reader.repairing;Cash_dispenser.repairing;Deposit_drawer.repairing;Receipt_printer.repairing