Abstract: The entrance guard system for bank vaults is an access control system that requires extremely strict security measures, which is the first secure perimeter in the vaults. The system usage process involves more multiple constraints and complicated procedure than a common one. Compared the two systems, it leads to the theorem that a sound WF-net is still sound after adding constraints. Workflow net is used to model the entrance guard system for the common scene and bank vaults. Then, YAWL Editor is used to analyze the system models. By the end of this paper, the system is implemented by the hardware-software co-design methodology. One application example is presented to illustrate the proposed system. The correctness of the theorem is verified and the use of workflow net effectively decreases the level of the system design complexity, ensures the validity of the design, and improves the efficiency of system development.

Key words: Petri nets, workflow net, YAWL Editor, entrance guard system, hardware-software co-design

摘要： 银行业务库门禁系统是一种对安全要求极高的出入口控制系统，作为业务库的第一道安全防线，该系统比普通门禁拥有更多的约束条件、更复杂的流程。先对比普通门禁和业务库门禁系统，由此引出定理合理的工作流网中加入约束后仍然是合理的工作流网。然后通过工作流网对普通门禁和业务库门禁系统进行了系统模型的建立，再采用YAWL Editor工具分析了所构建系统的正确性，最后使用软硬件协同设计的方法改进并实现了业务库门禁系统。实验结果验证了定理的正确性，同时表明基于工作流网的方法有效降低了门禁系统的设计难度，并在具体实现之前确保了设计的正确性，提高了系统的开发效率。

关键词: Petri网, 工作流网, YAWL Editor, 门禁系统, 软硬件协同设计