银行账户管理系统着色Petri网建模

一、建模架构

      本Colored Petri Nets用于为银行账户管理系统建模，架构为层次型着色Petri网，共分3层。

      顶层Page为Bank Management System，包含Login，Register，Query Balance，Transfer Accounts四个SubPage，分别实现登录、注册、查询余额、转账功能。

      二层SubPage Login实现登录功能，输入用户身份证号、密码，验证成功后，完成登录操作。

      二层SubPage Register实现注册功能，进入注册页面后，输入用户身份证号、用户名、用户密码、用户手机号，将信息记录入数据库，即可实现注册功能。

      二层SubPage Query Balance实现查询余额功能，接收传入的用户身份证号和银行卡号后，查询数据库，并显示余额。

      二层SubPage Transfer Accounts实现转账功能，接收传入的用户身份证号和银行卡号后，输入转账目标帐户的用户身份证号、银行卡号和转账金额，查询数据库目标帐户确实存在且信息输入无误后，执行转账操作。该转账操作又分三级子页SubPage Transfer Accounts Operation，如果转账成功，跳转回主页面，如果转账失败，重新转账。

      三层SubPage Transfer Accounts Operation具体实现转账操作，先向目标帐户增加转账金额，然后从原账户减少金额，若转账操作成功，报告转账成功，若转账操作失败，报告转账失败。

 

二、类型声明

       colset UNIT = unit;

       colset INT= int;

       colset BOOL = bool;

       colset STRING = string;

       colset UserPw = STRING;

       colset UserName = STRING;

       colset UserID = STRING;

       colset UserInfo = product UserID*UserPw;

       colset UserTel = STRING;

       colset BankCardID = STRING;

       colset BankCardInfo = product UserID*BankCardID;

       colset Result = with O|E;

       colset UserInfoAdv = product UserName*UserTel;

       colset UserInfoAll = product UserID*UserPw*UserName*UserTel;

       colset TargetUserID = STRING;

       colset TargetBankCardID = STRING;

       colset ForwardMoney = INT;

       colset BankCardInfoAll = product UserID*BankCardID*TargetUserID* TargetBankCardID*ForwardMoney;

       var UN:UserName;

       var UP:UserPw;

       var UI:UserID;

       var UT:UserTel;

       var TUI:TargetUserID;

       var TBCI:TargetBankCardID;

       var FM:ForwardMoney;

       var BCI:BankCardID;

       var VR:Result;

       var TR:Result;

       var AR:Result;

       var RR:Result;

 

三、每层页面具体分析

      （1）顶层Page：Bank Management System。

      该Page为顶层Page。位置Bank Management System的colset为UserInfo，具有初始Token：1`(“1234567890”,”888888”)。点击“银行账户管理系统”图标，系统启动，进入登录页面Login Page。如果此前没有注册，可以进行注册，注册成功，重新登录。如果此前已注册，可以直接登录。登录成功，进入主页面。主页面具有初始Token：1`(“1234567890”,”62250646839”)，主页面的colset为BankCardInfo。在主页面可以完成两个功能：查询余额和转账。查询余额或转账操作完成，返回主页面。若用户结束银行账户管理，可以登出，系统运行即宣告结束。

      （2）二层SubPage：Login。

      该Page用于实现登录功能。用户进入登录页面Login Page，输入身份证号、密码。系统根据输入查询数据库，并验证用户信息。如果验证成功，即跳转到主页面；如果验证失败，重新输入用户身份证号、密码，重新登录。

      （3）二层SubPage：Register。

      该Page用于实现注册功能。用户进入登录页面Login Page，点击“注册”按钮，进入注册页面，注册页面的colset为 UserInfoAdv，具有初始Token：1`(“Jack”,”0108542968”)。输入用户身份证号、用户名、用户密码、用户手机号，系统将信息插入数据库，即可完成注册操作。

      （4）二层SubPage：Query Balance。

      该Page用于实现查询余额功能。用户位于主页面Main Page，接收用户身份证号、用户银行卡号。系统查询数据库，并显示银行卡余额信息。查询余额结束，系统跳转到主页面。

      （5）二层SubPage：Transfer Accounts。

      该Page用于实现转账功能。用户位于主页面Main Page，接收用户身份证号、用户银行卡号。系统跳转到转账页面Transfer Accounts Page，转账页面具有初始Token：1`(“1234567890”,”62250646839”,”1023456789”,”62289045636”,200)。在转账页面输入目标用户身份证号、目标银行卡号、转账金额，系统查询数据库，核实目标帐户信息。如果目标账户信息输入有误，则重新输入目标账户信息。如果目标账户信息输入正确，则进行转账操作Transfer
Accounts Operation，转账操作具有SubPage Transfer Accounts Operation。如果转账失败，重新接收用户身份证号、用户银行卡号，重新转账。如果转账成功，系统跳转回主页面。

      （6）三层SubPage：Transfer Accounts Operation。

      该Page用于具体实现转账操作。目标账户信息核实成功之后，先向目标账户增加转账金额。如果增加失败，报告转账失败。如果增加成功，则再从原账户减少转账金额。如果减少失败，报告转账失败。如果减少成功，报告转账成功。

 

四、颜色标识

      （1）粉色：colset为UserInfo的位置。

      （2）红色：colset为BankCardInfo的位置。

      （3）紫色：colset为UserInfoAdv的位置。

      （4）深红色：colset为BankCardInfoAll的位置。

      （5）蓝色：出现Error的位置。

      （6）棕色：结束位置。

      （7）绿色：普通变迁。

      （8）青色：替代变迁。

五、Colored Petri Nets截图如下：

      （1）顶层Page：Bank Management System。



      （2）二层SubPage：Login。



      （3）二层SubPage：Register。



      （4）二层SubPage：Query Balance。



      （5）二层SubPage：Transfer Accounts。





      （6）三层SubPage：Transfer Accounts Operation。