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 here (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