基于PI-演算的网上并联审批业务流程建模及验证

　　摘要：首次将进程代数pi演算理论引入电子政务流程建模中，对电子政务研究中的热点、难点，即网上并联审批流程进行了形式化建模，并对所建立的模型进行了验证，确保了模型的正确性和可行性，极大地降低了项目实施投资风险。
　　关键词：电子政务； 流程建模； 模型验证； pi演算； 进程

　　0引言
　　
　　近年来，世界各国在提倡和推进信息化战略中都把电子政务作为首要任务。推进政府部门办公自动化、网络化、电子化已是大势所趋。国内各级政府都在大力推进信息化建设。政府的组织形态也正由职能型向服务型转变[1]；政府的行政业务正由传统的方式向信息化方向转变。中国政府的电子政务经过前期的投资建设已经具备了一定的硬件设施和软件环境。但是政府各部门之间联合审批事项数据始终不能共享，这使得数据共享和协同工作成为我国电子政务发展过程中要解决的关键问题。行政许可法的颁布给基于业务流程为核心驱动的跨部门联合行政审批带来了挑战和契机，跨组织、跨部门、跨区域的网上关联审批成为了目前研究的热点和难点。
　　网上并联审批是应用web技术，把分布在不同部门、不同区域的已有、将有的政府信息资源迅速整合成为一种没有（或很少有）时间和空间的制约，以信息通信手段实现政府跨部门协作和统一审批的信息系统。要实施网上并联审批系统第一步工作是根据应用要求设计业务流程，也称为流程建模。要完成网上并联审批的电子化和网络化，准确地构建电子政府的业务模型是十分关键的一步。流程建模合理与否决定政务项目的成败。
　　前期用于政府业务建模的技术有工作流图、uml[2]、petri网、bpms等。uml是面向对象开发中的一种通用而又统一的图形化模型语言。uml建模形式简单易懂，但缺乏形式化语义基础，模型检测性差。工作流技术(workflow)早期主要用于描述工业及办公自动化，对工作过程约束条性太强，灵活性较差，较适用于一些相关规范、稳定不变的业务流程。即使工作流管理联盟全新定义了工作流[3,4]，但是大规模过程操作中隐含着错误[5]。petri 网技术具于丰富的语义定义、坚实的数学理论和直观的图形化界面，是目前构建工作流模型较为理想的建模方法[6,7]。但对于复杂系统的流程模型描述有一定的局限性[8]。bpm[9,10]被smith、fingar称为业务流程管理的第三次浪潮。它是一种以规范化的构造端到端，以持续提高组织业务绩效为目的的卓越业务流程管理方法。bpm的关键是将业务流程计算机模型化、标准化，将业务流程与业务应用相分离。bpm的技术实现被称为业务流程管理系统(bpms)。bpms[11]的技术基础是工作流管理系统(wfms)、企业应用集成(eai)、电子商务等。bpms的理论基础是进程代数pi演算[12~15]。pi演算比传统工作流模型更加灵活、理论性更强，能描述复杂系统，支持结构变化的动态系统，提供安全控制，支持信息的异步并发性，将计算机的计算和通信两种基本功能进行统一，从而能协调分布式业务流程。
　　本文首次引入进程代数pi演算理论到电子政务建模中，对复杂的、动态变化的、并发运行的网上并联审批系统进行了形式化建模，并对所建模型的合理性、可行性进行了分析验证；确保了模型的正确性，避免了模型实施过程发现错误的修改周期长、代价大等缺陷，确保了政府部门项目的成功率，极大地降低了政府项目投资风险。
　　

　　用死锁检验命令deadlocks检验流程p是否有死锁。结果是没有死锁。用交互模拟step命令运行流程p。结果是流程p的每一步运行过程，如申办人与工商系统的通道是什么及通道上的信息是什么等。这有利于分析、检查整个流程的每一步交互是否按设计过程在运行，等等。
　　在应用pi演算理论对网上并联审批业务流程所建模型验证及推理过程、跟踪分析、检验业务流程中，发现了描述过程中不合理部分，修正后使模型更具有合理性、实用性，确保了项目的可行性，从而避免了模型实施后错误修改周期长、代价大等缺陷，极大地降低了政府项目投资风险，提高了项目的成功率。
　　
　　4结束语
　　
　　政府网上并联审批业务流程系统是电子政务研究的热点方向。本文首次把pi演算理论引入到电子政府中来，为政府业务系统长远建设发展作了初步的探索。pi演算对政府网上并联审批业务流程的信息交互进行了精确的抽象描述，并对整个业务流程进行了验证，政府投资的风险大大降低了。它为政府跨部门、跨区域信息交互提供了新的思路和方法。
　　下一步工作中，以pi演算为理论基础开发业务流程图形化管理软件，将实现图形化描述与进程代数验证自动双向转换。应用pi演算等互模、强互模、弱互模、观察互模等理论，近一步分析及优化业务流程，从而推动电子政务的发展。
　　
　　参考文献：
　　［1］孟庆国,樊博.电子政务理论与实践[m].北京：清华大学出版社,2006.
　　［2］徐宝文, 周毓明, 卢红敏.uml与软件建模[m].北京:清华大学出版社，2006.
　　［3］georgakopolous d，hornick m， sheth overview of workflow management:from process modeling to workflow automation infrastructure[j].distributed and parallel databases,1995,3(2):119153.
　　［4］workflow management ow management coalition terminology and glossary,wfmctc1011[s].brussels:wfmc,1996.
　　［5］aalst w. finding control flow errors using petrinetbase techniques[m]//aalst w, desel j, oberweis ss process mangement:models,techniques, and empirical studies. berlin: springerverlag, 2000:161183.
　　［6］李红臣, 史美林. 工作流模型及其形式化描述[j]. 计算机学报,2003,26(11):14561463.
　　［7］aalst w van der. hee k van. 工作流管理模型、方法和系统[m]. 王建民, 闻立杰，等译.北京：清华大学出版社, 2004.
　　［8］aalst w m p van der. picalculus versus petri nets: let us eat “humble pie”, rather than further inflate the “pi hype”[j]. bptrends, 2005,3(5)：111. 　　 ［9］smith h, fingar p. business process management:the third wave [m]. tampa: meghankiffer press, 2003:1-312.
　　［10］smith ss process managementthe third wave:business process modeling language (bpml) and its picalculus foundations[j]. information and software technology,2003,45:10651069.
　　［11］smith h, fingar p. workflow is just a pi process[eb/ol]. (2004-01).http:.
　　［12］milner r. communicating and mobile systems: the πcalculus[m].cambridge:cambridge university press,1999:1161.
　　［13］milner polyadic πcalculus:a tutorial[m]//logic and algebra of specification. berlin :springerverlag,1993:1-50.
　　［14］sangiorgi d,walker d. the πcalculus: a theory of mobile processes[m]. cambridge: cambridge university press,2001:1-580.
　　［15］milner r,parrow j,walker d. a calculus of mobile processes ⅰ,ⅱ[j].inf comput, 1992,100(1):1-40,41-77.
　　［16］milner r. communication and concurrency[m]. englewood cliffs, nj:prentice hall international,1989:1-260.
　　［17］陈禹六.idef 建模分析和设计方法[m].北京 :清华大学出版社,1999.