1、64 电子技术 第 52 卷 第 5 期（总第 558 期）2023 年 5 月Computer Engineering计算机工程0 引言云物流是将所有管理机构、代理商、物流公司等都集中云整合成资源池，在各个资源之间根据需求进行交流，从而达到提高效率、降低成本的目的，实现物流配送的效率最大化。1 研究背景防疫优化措施出台，对于科学精准抓好疫情常态化防控提出了更高的要求。每个公民要自觉服从防控需要，做好自身防护。同时，如果出现咳嗽、发热等症状，我们就需要居家并对症处置或口服药物治疗。符合居家医疗指南居家的，凭借在线开具的处方，并鼓励符合条件的第三方配送药品。疫情常态化防控阶段对药品物流提出了更高
2、的要求。长期以来，我国的药品物流主要由大型医药流通企业建设医药物流配送中心，或者由有资质的第三方医药物流企业来承担物流配送服务1。但由于信息技术应用投入缺乏，药品物流信息不能及时共享，导致成本高，运营效率低。目前，众多学者已对云物流和医药物流问题进行了研究，文献2建立药品云配送平台，并提出了云物流网络配送模式。文献3将“云计算”和“物联网”相结合，构建了“云计算”智慧医药物流体系。文献4对云物流应用于快递行业的依据做出详细的解析。2 Pi演算理论Pi演算由Robin Milner在1990年提出的一种形式化模型的方法5。Pi演算可以传递通道名、变量及值，常用于描述具有并行性、交互性的系统。因此
3、，使用Pi演算来对药品云物流系统这种需要并发运算的系统进行描述是非常适合的。进程及名字是Pi演算中最基本的两个实体单位，可以用x、y、z等英文字母表示名字，用X、Y、Z等来指代进程。常见的进程表达式如下。（1）P:=0，表示空进程。（2）P，表示如果变量x和变量y匹配就执行后续进程P。（3）(!P)，表示连续执行进程P。（4）P1|P2，表示进程P1和进程P2可以单独执行，也可以同时运行。（5）P1+P2，仅执行进程P1或者进程P2。（6），通道y发送名字x，再执行进程P。（7），通道y接收名字x，再执行进程P。（8），表示进程P中的变量x是进程P的约束名。作者简介：刘峰，山西医科大学汾阳学院
4、；研究方向：智能算法应用。收稿日期：2022-12-20；修回日期：2023-05-12。摘要：阐述Pi演算来推演药品云物流系统的交互行为，形式化验证了交互行为的可靠性及安全性。设计出的模型可为实际系统的设计开发提供参考和依据。使用药品云物流系统可以提高效率、降低成本。关键词：药品云物流系统，Pi 演算，形式化验证。中图分类号：TP311.13，TP18文章编号：1000-0755(2023)05-0064-03文献引用格式：刘峰.基于Pi演算的药品云物流业务流程建模分析J.电子技术,2023,52(05):64-66.基于Pi演算的药品云物流业务流程建模分析刘峰（山西医科大学汾阳学院，山西
5、032200）Abstract This paper describes Pi calculus to deduce the interaction behavior of the pharmaceutical cloud logistics system,and formally verifies the reliability and security of the interaction behavior.The designed model can provide reference and basis for the design and development of the act
6、ual system.The use of pharmaceutical cloud logistics system can improve efficiency and reduce costs.Index Terms pharmaceutical cloud logistics,Pi calculus,formal verification.Analysis of Business Process Modeling of Drug Cloud Logistics Based on Pi CalculusLIU Feng(Fenyang College of Shanxi Medical
7、University,Shanxi 032200,China.)电子技术 第 52 卷 第 5 期（总第 558 期）2023 年 5 月 65Computer Engineering计算机工程3 药品云物流系统业务流程分析随着社会经济的发展和国家政策的支持，云物流必将成为未来物流发展的最佳选择。药品云物流系统能把各种资源进行整合，使得系统能够合理调配药品、物流等各种资源，不但降低了服务成本，还提高了运营效率。实体药店、药品生产企业将药品信息发布在药品云物流系统，购买人通过系统查询到所需药品，同时可以对药品价格进行对比，选择自己认为最合理的购买方式。当药品可以在就近的药店购买时，系统根据距离推
8、送出实体药店供购买人选择。实体药店、药品生产企业可以通过药品云物流系统及时收集购买人的需求，从而对药品的生产进行充足的调整，有特别需求的药品可以尽快生产投入市场，需求量不是特别大的药品可以降低生产量，从而保证企业或药店成本的可调、可控。通过药品云物流系统，可以随时查询物流公司、订单等信息，信息透明及时，尽可能提供好的服务体验。3.1 基于BPMN的药品云物流流程图业务流程管理组织（BPMI）开发制定了业务流程建模标记（BPMN）标准6。BPMN提供了容易理解且易于描述的建模符号，方便业务流程中的参与者对业务流程进行建模。同时也提供了直观的图形设计界面，业务流程中的参与者可以将所需描述的业务流程
9、展示出来。通过对药品云物流系统的流程分析，可通过BPMN将系统中的交互以图像的形式描述出来，如图1所示。3.2 药品云物流系统形式化描述上面使用BPMN2.0给出了药品云物流系统业务交互的流程图，但BPMN并不能对流程进行形式化分析，因此使用Pi演算对该编排进行描述，从而验证构造模型是否正确。根据Pi演算描述规则，结合药品云物流业务流程图给出如下几个定义。定义1，交互中的消息集 News=browse,result,sell,sendrug,submit,drugout,sendaccomplish,onlinepay,sendgoods其中，browse：浏览查询药品；result：云物流系
10、统反馈查询结果；sell：线下最近的商店销售药品；sendrug：从药厂发货；submit：顾客提交订单；drugout：药品出库；sendaccomplish：交易完成；onlinepay：在线支付；sendgoods：配送药品。定义2，各部门之间的传输通道集 Channels=sg,ds,so,op,dg,sa,gd,do,sr通过如上的定义，得到Pi演算模型，具体如图2所示。图1 药品云物流系统协作流程图66 电子技术 第 52 卷 第 5 期（总第 558 期）2023 年 5 月Computer Engineering计算机工程4 基于MWB的模型验证移动工作台MWB（Mobilit
11、y Wordbench）是Pi演算的分析工具，可以通过命令行方式分析与验证Pi演算所描述的并发系统，能够对流程中是否存在死锁和对活动进行流程模拟。将Pi演算的形式化代码转换为MWB能够识别的代码，然后将代码使用MWB工具进行流程模拟及验证死锁。（1）第一步：将MWB工具安装，双击smlnj.exe并默认安装到C盘中sml文件夹中。（2）第二步：将mwb.x86-win32和mwb.bat复制到sml文件夹中。（3）第三步：双击mwb.bat运行MWB工具。加载文件pcl.ag。输入input“pcl.ag”，当文件中的代理都正确时，如图3所示。（4）第四步：验证死锁。输入deadlocks p
12、cl，验证药品云物流系统pcl是否存在死锁。该流程显示No deadlocks found,说明该流程交互正确，无死锁。5 结语本文应用Pi演算来推演药品云物流系统的交互行为，可为实际系统的设计开发提供参考和依据，降低后期系统研发过程中可能会出现的死锁等情况，节约了成本。由于购买人在购药过程中会出现多种情况，本文的模型具有一定局限，今后将结合实际进行模型优化，更好提高系统的有效性。参考文献1 黄惠春,邓冬梅.“互联网+”药品云物流架构和商业模式的研究J.现代商业,2018(07):14-15.2 汪传雷,陈娇,王栋梓.基于物流4.0的药品云配送模式研究J.北华大学学报(社会科学版),2015,
13、16(04):33-37.3 杨玮,党培.基于云计算的医药冷链物流体系构建J.制造业自动化,2014,36(24):6-9.4 杜晓娟.基于云计算的云物流在快递行业中的应用J.浙江万里学院学报,2014,27(02):28-31+35.5 MILNER R.Communication and Mobile systems:the Pi-CalculusM.Berlin:Cambridge University Press,1999.6 Object Management Group.Business process modeling notation(BPMN)version 1.2R.Technical report,2009.图2 Pi演算模型图3 导入代码
