基于Pi-演算的无线自动售货机系统建模与应用
|
摘要
无线自动售货机系统通过无线网络实现了对自动售货机的远程监视和控制,便于企业内部物流管理及向顾客提供方便的手机购物。为了对这一复杂系统形成一致的理解,分析系统的正确性和可靠性,进而定量评估系统的绩效,需要建立一种严谨的可模拟系统动态运行的模型。
由于无线自动售货机系统属于离散动态系统,本文采用了描述分布式并发系统的Pi-演算过程代数方法为系统建模。分别对系统的交易流程和物流配送过程建立了Pi-演算模型。对无线自动售货机系统的交易流程的建模采用自顶向下的建模方法,首先建立系统的主要活动模块的顶层Pi-演算模型,然后对这些模块进行细化,最后得出系统交易流程完整的Pi-演算模型;并用Pi-演算的形式化辅助工具MWB验证其正确性。为了能够对无线自动售货机系统物流配送过程进行建模,本文定义了一种带时间因素的Pi-演算,对无线自动售货机系统的物流配送过程建立了含有时间因素的Pi-演算模型;考虑到绩效分析的需要,还在不同的缺货情况下同时模拟两种系统物流配送过程的运行,通过选择最佳的配送路线,得出无线售货机物流配送过程与传统售货机物流配送过程工作效率的提高。
本文为系统复杂的交易流程和物流配送过程建立了精确的Pi-演算模型,使系统的开发人员、监控人员和维护人员对系统形成了一致的准确的理解,为系统的分析和改进打下良好基础。同时对系统物流配送过程进行量化,实现了无线自动售货机系统的时间绩效分析。
Wireless vending machine system realizes the long-distance control, it is convenient for enterprise to manage the distribution, also easy to be shopping by phone for customers. To reach an agreement on the complicated system unanimously, analyze reliability and the efficiency amelioration of wireless system, finding an accurate model that can model the system dynamically is a necessary.
Wireless vending machine system belongs to the discrete event dynamic system, Pi-Calculus which is a kind of the process algebra can analyze and model the system that has characteristics as concurrent and resource sharing usefully. Pi-Calculus modeling technology is applied to model and research the wireless vending machine system to model the business process and the logistics distribution process. The modeling method called "from top to bottom" is to model business process. The top Pi-Calculus model is built aiming at the main activities modules of the system. And then the integrated Pi-Calculus model of business process is found, at one time, through executing on the simulator MWB to prove the changed structure of the serve. A timed Pi-Calculus model with time is defined to model the logistics distribution process of the wireless system in a definite distribution environment. Considered the need of performance analysis, the model of the logistics distribution process of the traditional vending machine system is found too. These two models are simulated in different situations.
In this paper an accurate Pi-Calculus model is built for the business process of the system, can make the personnel of the system to form a uniform and exact comprehend and ground a well foundation for the analysis and improvement of the system. The modeling for the logistics distribution process of the wireless system quantifies the efficiency amelioration of wireless system and realizes the time performance analysis of the wireless vending machine system.
由于无线自动售货机系统属于离散动态系统,本文采用了描述分布式并发系统的Pi-演算过程代数方法为系统建模。分别对系统的交易流程和物流配送过程建立了Pi-演算模型。对无线自动售货机系统的交易流程的建模采用自顶向下的建模方法,首先建立系统的主要活动模块的顶层Pi-演算模型,然后对这些模块进行细化,最后得出系统交易流程完整的Pi-演算模型;并用Pi-演算的形式化辅助工具MWB验证其正确性。为了能够对无线自动售货机系统物流配送过程进行建模,本文定义了一种带时间因素的Pi-演算,对无线自动售货机系统的物流配送过程建立了含有时间因素的Pi-演算模型;考虑到绩效分析的需要,还在不同的缺货情况下同时模拟两种系统物流配送过程的运行,通过选择最佳的配送路线,得出无线售货机物流配送过程与传统售货机物流配送过程工作效率的提高。
本文为系统复杂的交易流程和物流配送过程建立了精确的Pi-演算模型,使系统的开发人员、监控人员和维护人员对系统形成了一致的准确的理解,为系统的分析和改进打下良好基础。同时对系统物流配送过程进行量化,实现了无线自动售货机系统的时间绩效分析。
Wireless vending machine system realizes the long-distance control, it is convenient for enterprise to manage the distribution, also easy to be shopping by phone for customers. To reach an agreement on the complicated system unanimously, analyze reliability and the efficiency amelioration of wireless system, finding an accurate model that can model the system dynamically is a necessary.
Wireless vending machine system belongs to the discrete event dynamic system, Pi-Calculus which is a kind of the process algebra can analyze and model the system that has characteristics as concurrent and resource sharing usefully. Pi-Calculus modeling technology is applied to model and research the wireless vending machine system to model the business process and the logistics distribution process. The modeling method called "from top to bottom" is to model business process. The top Pi-Calculus model is built aiming at the main activities modules of the system. And then the integrated Pi-Calculus model of business process is found, at one time, through executing on the simulator MWB to prove the changed structure of the serve. A timed Pi-Calculus model with time is defined to model the logistics distribution process of the wireless system in a definite distribution environment. Considered the need of performance analysis, the model of the logistics distribution process of the traditional vending machine system is found too. These two models are simulated in different situations.
In this paper an accurate Pi-Calculus model is built for the business process of the system, can make the personnel of the system to form a uniform and exact comprehend and ground a well foundation for the analysis and improvement of the system. The modeling for the logistics distribution process of the wireless system quantifies the efficiency amelioration of wireless system and realizes the time performance analysis of the wireless vending machine system.
引文
[1]Gu Hong,Qiao Shuang,Tian Jiang.A Wireless Vending Machine System Based on GSM.The sixth world congress on intelligent control and automation,2006,volume 10 of 12:8501-8504.
[2]Choi SY.电子商务经济学.北京:电子工业出版社,2000:9.
[3]Milner R.Communicating and Mobile Systems:The Pi-Calculus.Cambridge:Cambridg University Press,1999.
[4]Lin Huimin.Complete proof systems for observation congruences in finite control Pi-Calculus.In:Proceedings of the 25th International Colloquium on Automata.Languages and Programming.Denmark:Aalborg,1998:443-454.
[5]Jiao Wenpin,Zhou Minghui,Wang Qianxiang.Formal framework for adaptive multi agent Systems.In:Proceedings of IEEE/WIC International Conference on Intelligent Agent Technology.Canada:Halifax.2003:442-445
[6]Markus L.A Pi-Calculus based approach to software composition(Ph.D.dissertation).Institute of Computer Science and Applied Mathematics:University of Bern,Switzerland,1999.
[7]傅铅生,王建玲.如何开拓移动电子商务市场.商业时代,2005,11(3):63-65.
[8]季元,刘武韬,赵飞龙.不断飞速发展的信息技术——SMS.中国数据通信,2002,10:55-59.
[9]Qiao Shuang,Gu Hong.An analysis on success factors of M-commerce applications.Proc of 2005 ICMSE,2005,1:172-176.
[10]陈安宝.基于手机短信应答的自动售货机.科技情报开发与经济,2004,14(9):263-264.
[11]柳赛虎,唐立,高建龙.手机自动售货机的嵌入式系统设计.单片机与嵌入式系统应用,2006,2:56-59.
[12]郑大宇,王巍.基于网络的自动售货机的实现方法.哈尔滨商业大学学报(自然科学版),2005,21(6):768-771.
[13]詹昌平,金瓯.基于移动支付的自动售货机.现代电子技术(自动化技术),2004,17:38-40.
[14]姜爱丽.基于Petri网的无线自动售货机系统的建模与应用研究:(硕士论文).大连:大连理工大学,2007.
[15]Giacomo GD,Lesperance Y,Levesque HC.A Concurrent Programming Language based on the Situation Calculus.Artificial Intelligence.,2000,121(2):109-169.
[16]吴哲辉.Petri网导论.北京:机械工业出版社,2006:4.
[17]黄海新,汪定伟.基于过程代数的商务过程重组方法.管理工程学报,2002,16(4):60-63.
[18]Baeten JM,Weijland WP.Process Algebra.New York:Cambridge University Press,1990.
[19]Hoare C.Communicating Sequential Processes.Upper Saddle River:Prentice Hall,1985.
[20]Milner R.A Calculus of Communicating Systems.New York:Springer,1980.
[21]Bolognesi T,Brinksma E.Introduction to the ISO specification language LOTOS.Computer Networks and ISDN Systems,1987,14(1):25-59.
[22]Ho YC,Cassandras CG.A new approach to the analysis of discrete event dynamic systems.Automatica,1983,19(2):149-167.
[23]曹希仁.离散事件动态系统.自动化学报,1985,11(4):438-446.
[24]郑大钟,郑应平.离散事件动态系统理论的现状和展望.自动化学报,1992,18(2):139-142.
[25]Ranadge R,Wonham PJ.Supervisory control of a class of discrete event processes.Control and Optimization,1987,25(1):206-230.
[26]郑应平.离散事件系统理论研究和应用进展.控制与决策,1996,11(2):233-241.
[27]钱军,冯玉琳.系统动态行为语义模型及其形式描述.计算机研究与发展,1999,36(8):907-914.
[28]Xavier N,Joseph S.An Overview and Synthesis on Timed-Process Algebras.The 3rd Workshop on Computer Aided Verification.Denmark:Aalborg,1991:1-21.
[29]Baeten J.A Brief History of Process Algebra.Theoretical Computer Science.,2005,335(2):131-146.
[30]Hennessy M,Lin H.Symbolic Bisimulations.Theoretical Computer Science,1995,138(2):353-389.
[31]Lin H.A Verification Tool for Value-Passing Processes.13th IFIP Symposium on Protocol Specification,Testing and Verification,Belgium:Liege,1993.C-16(5):79-92.
[32]Milner R,Parrow J,Walker D.A calculus of mobile processes,part Ⅰ/Ⅱ.Journal of Information and Computation,1992,100(1):1-77.
[33]王永祥,吴尽昭,将建民.进程代数—对称与动作细化.北京:科学出版社,2007:6.
[34]江海昇,范辉.USSD对话有限状态自动机的设计与实现.计算机应用,2005,25(9):2199-2201.
[35]陈宣励,崔锦秀.USSD系统与应用简介.广西通信技术,2004,24(3):18-22
[36]李伟.关于USSD系统建设几点看法.黑龙江省通信学会学术年会.2005:364-368.
[37]刘威,武家春.非结构化补充业务数据中心的设计与实现.计算机工程与应用.2005,68(10):1-7.
[38]乔非,吴启迪,沈荣芳.面向企业流程重建的事物流程模型研究与应用.系统工程理论与实践,1999,23(1).
[39]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证.计算机学报,2005,28(4):635-643
[40]Frank P,Mathias W.Using the π-calculus for formalizing workflow patterns,van der Aalst,W.Proceedings of 2005 International conference on business process management.Berlin:Springer,2005,13(6):153-168.
[41]廖军,谭浩,刘锦德.基于Pi-演算的Web服务可替换性验证.华中科技大学学报,2005,28(4):168-171.
[42]Koshkina M,Breugel F.Modelling and verifying Web service orchestration by means of the concurrency workbench.ACM SIGSOFT SEN,2004,29(5):1-10.
[43]乔爽,张春成,顾宏.基于π-演算的移动商务过程形式化描述和验证.计算机工程与应用,2006,32(21):167-173.
[44]乔爽,张春成,顾宏.基于时间PI-演算的移动商务过程建模.管理工程学报,2007,13(4):121-126.
[2]Choi SY.电子商务经济学.北京:电子工业出版社,2000:9.
[3]Milner R.Communicating and Mobile Systems:The Pi-Calculus.Cambridge:Cambridg University Press,1999.
[4]Lin Huimin.Complete proof systems for observation congruences in finite control Pi-Calculus.In:Proceedings of the 25th International Colloquium on Automata.Languages and Programming.Denmark:Aalborg,1998:443-454.
[5]Jiao Wenpin,Zhou Minghui,Wang Qianxiang.Formal framework for adaptive multi agent Systems.In:Proceedings of IEEE/WIC International Conference on Intelligent Agent Technology.Canada:Halifax.2003:442-445
[6]Markus L.A Pi-Calculus based approach to software composition(Ph.D.dissertation).Institute of Computer Science and Applied Mathematics:University of Bern,Switzerland,1999.
[7]傅铅生,王建玲.如何开拓移动电子商务市场.商业时代,2005,11(3):63-65.
[8]季元,刘武韬,赵飞龙.不断飞速发展的信息技术——SMS.中国数据通信,2002,10:55-59.
[9]Qiao Shuang,Gu Hong.An analysis on success factors of M-commerce applications.Proc of 2005 ICMSE,2005,1:172-176.
[10]陈安宝.基于手机短信应答的自动售货机.科技情报开发与经济,2004,14(9):263-264.
[11]柳赛虎,唐立,高建龙.手机自动售货机的嵌入式系统设计.单片机与嵌入式系统应用,2006,2:56-59.
[12]郑大宇,王巍.基于网络的自动售货机的实现方法.哈尔滨商业大学学报(自然科学版),2005,21(6):768-771.
[13]詹昌平,金瓯.基于移动支付的自动售货机.现代电子技术(自动化技术),2004,17:38-40.
[14]姜爱丽.基于Petri网的无线自动售货机系统的建模与应用研究:(硕士论文).大连:大连理工大学,2007.
[15]Giacomo GD,Lesperance Y,Levesque HC.A Concurrent Programming Language based on the Situation Calculus.Artificial Intelligence.,2000,121(2):109-169.
[16]吴哲辉.Petri网导论.北京:机械工业出版社,2006:4.
[17]黄海新,汪定伟.基于过程代数的商务过程重组方法.管理工程学报,2002,16(4):60-63.
[18]Baeten JM,Weijland WP.Process Algebra.New York:Cambridge University Press,1990.
[19]Hoare C.Communicating Sequential Processes.Upper Saddle River:Prentice Hall,1985.
[20]Milner R.A Calculus of Communicating Systems.New York:Springer,1980.
[21]Bolognesi T,Brinksma E.Introduction to the ISO specification language LOTOS.Computer Networks and ISDN Systems,1987,14(1):25-59.
[22]Ho YC,Cassandras CG.A new approach to the analysis of discrete event dynamic systems.Automatica,1983,19(2):149-167.
[23]曹希仁.离散事件动态系统.自动化学报,1985,11(4):438-446.
[24]郑大钟,郑应平.离散事件动态系统理论的现状和展望.自动化学报,1992,18(2):139-142.
[25]Ranadge R,Wonham PJ.Supervisory control of a class of discrete event processes.Control and Optimization,1987,25(1):206-230.
[26]郑应平.离散事件系统理论研究和应用进展.控制与决策,1996,11(2):233-241.
[27]钱军,冯玉琳.系统动态行为语义模型及其形式描述.计算机研究与发展,1999,36(8):907-914.
[28]Xavier N,Joseph S.An Overview and Synthesis on Timed-Process Algebras.The 3rd Workshop on Computer Aided Verification.Denmark:Aalborg,1991:1-21.
[29]Baeten J.A Brief History of Process Algebra.Theoretical Computer Science.,2005,335(2):131-146.
[30]Hennessy M,Lin H.Symbolic Bisimulations.Theoretical Computer Science,1995,138(2):353-389.
[31]Lin H.A Verification Tool for Value-Passing Processes.13th IFIP Symposium on Protocol Specification,Testing and Verification,Belgium:Liege,1993.C-16(5):79-92.
[32]Milner R,Parrow J,Walker D.A calculus of mobile processes,part Ⅰ/Ⅱ.Journal of Information and Computation,1992,100(1):1-77.
[33]王永祥,吴尽昭,将建民.进程代数—对称与动作细化.北京:科学出版社,2007:6.
[34]江海昇,范辉.USSD对话有限状态自动机的设计与实现.计算机应用,2005,25(9):2199-2201.
[35]陈宣励,崔锦秀.USSD系统与应用简介.广西通信技术,2004,24(3):18-22
[36]李伟.关于USSD系统建设几点看法.黑龙江省通信学会学术年会.2005:364-368.
[37]刘威,武家春.非结构化补充业务数据中心的设计与实现.计算机工程与应用.2005,68(10):1-7.
[38]乔非,吴启迪,沈荣芳.面向企业流程重建的事物流程模型研究与应用.系统工程理论与实践,1999,23(1).
[39]廖军,谭浩,刘锦德.基于Pi-演算的Web服务组合的描述和验证.计算机学报,2005,28(4):635-643
[40]Frank P,Mathias W.Using the π-calculus for formalizing workflow patterns,van der Aalst,W.Proceedings of 2005 International conference on business process management.Berlin:Springer,2005,13(6):153-168.
[41]廖军,谭浩,刘锦德.基于Pi-演算的Web服务可替换性验证.华中科技大学学报,2005,28(4):168-171.
[42]Koshkina M,Breugel F.Modelling and verifying Web service orchestration by means of the concurrency workbench.ACM SIGSOFT SEN,2004,29(5):1-10.
[43]乔爽,张春成,顾宏.基于π-演算的移动商务过程形式化描述和验证.计算机工程与应用,2006,32(21):167-173.
[44]乔爽,张春成,顾宏.基于时间PI-演算的移动商务过程建模.管理工程学报,2007,13(4):121-126.