Banking system

Preamble

Banking system is a software case study, which is implemented in PauWare engine. The description of the case study (in French) is available here.

Resources

Installation requirements (Swing version)

User interface in Swing

Installation requirements (JavaFX version)

User interface in JavaFX

Specification of devices and Transaction (blue states are (initial) active states at simulation time)

        

Specification of ATM

Full-size SVG image may be found at the end of this Web page.

ATM

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