面向无线网络的形式化方法研究
|
摘要
无线网络己经被广泛运用于人们日常生活中的许多方面。尤其是在缺少固定基础设施的情况下,无线网络和无线技术是合适的通信解决方案,并且正在被广泛应用于实现信息传输的各种通讯场景中。构成无线网络的基础物理器件是无线网络节点设备,这些无线节点设备为无线网络应用的实现提供了基础的通信功能。
无线网络节点设备通常是以无线电波为载体进行广播式的信息发送,这种无线网络的广播信息发送模式与传统的有线以太网络中的全局广播信息发送模式有所不同。在无线网络中,信息数据的广播发送是局部的,也就是说每个无线节点所发送的信息的传输范围是有限的,只有那些处于节点传输半径覆盖范围内的部分接收节点才能够接收到所对应的节点广播发送的信息。受限于有限的信息传输范围,为了使得不在传输范围内的两个无线节点之间能够实现交互,就需要借助其他的中间节点来建立起一条能够传输信息的路由路径。路由协议是实现无线网络中路由路径的建立和维护的一种重要机制,主要是通过各种报文信息在无线网络中的广播来建立路由路径。
形式化方法被认为是对无线网络系统进行描述和验证的一种可行并且合适的方式。本文研究面向无线网络系统的形式化方法。我们主要研究无线网络中与通信交互相关的无线网络特性,包括无线节点之间的广播通信交互行为以及无线网络中路由协议建立路由路径的机制。
无线网络中无线节点之间的通信实现了无线网路中最根本的信息交互功能。我们考虑无线广播通信的各种物理特征,包括了无线节点的位置、通信范围、通信频率等物理因素。针对通信交互等无线节点底层物理行为的形式化描述和建模通常采用基于通信交互的进程代数演算系统。因此,我们扩展无线系统演算引入无线网络卫兵选择的概念,基于程序统一理提出了无线演算系统的代数语义和指称语义。我们给出了一系列无线系统演算的代数规则,研究从代数语义计算推导出操作语义的方法。
无线网络中的路由协议借助无线节点之间的通信交互实现了无线网络中的全局信息交互。针对无线网络中路由协议在路由建立和维护路由路径时的特点,我们主要考虑路由协议实现路由时的各种路由信息数据的处理机制。因此我们采用形式化描述语言对无线网络AODV路由协议进行形式化建模、分析和验证工作并且将底层的无线节点的通信交互行为抽象为针对变量的赋值效果。通过使用这种在更高层次的抽象描述方式,我们能够更直接地分析无线网络路由协议的本质特性。
本文的主要贡献包括：
·我们提出了无线系统演算的代数语义,给出了一组用于描述无线系统演算并行组合线性展开的代数规则,并且定义了无线网络系统的规范型。借助无线网络系统的规范型,我们给出了从代数语义计算生成操作语义的方法,并且证明了代数语义和操作语义的一致性,从代数语义的角度保证了操作语义的正确性和完备性。我们使用重写逻辑工具Maude实现了从代数语义自动计算操作语义的过程。我们提出了无线系统演算的指称语义,引入了无线网络执行状态和执行轨迹的概念用来描述无线网络的行为。基于指称语义模型,我们证明了无线网络系统的代数性质。
·我们使用形式化建模语言Z对无线网络中使用的AODV路由协议进行建模,并且使用基于Rely/Guarantee方法的形式化验证技术证明了协议的性质。通过形式化建模语言,我们在建模过程中消除了路由协议相关文档中自然语言描述的二义性。我们使用程序变量赋值的效果来描述无线节点之间的通信交互。我们对使用形式化语言Z构建的协议模型进行重写得到基于共享变量并行程序语言的改进协议模型。以共享变量并行程序所描述的路由协议形式化模型为基础,我们使用Rely/Guarantee推理规则证明了路由协议建立的路由路径不存在路由环路等性质。
Wireless networks have become prevalent relatively recently in our daily life. Wireless networks and applications are suitable solutions and being deployed in a wide range of communication scenarios, especially in infrastructurcless situations. Wireless devices are the basic components of wireless networks, which provide basic functions of communication and implement applications in wireless networks.
Wireless devices communicate with each other by broadcasting messages, which is quite different from the more conventional wired-based broadcast in Ethernet systems. Broadcast in wireless networks is local, i.e., a transmission covers a limited range and only a subset of all the devices in the network can receive the broadcasted message. Due to the limited transmission range of wireless devices, two remote wireless devices cannot communicate with each other directly. In order to transfer messages to a wireless device from a distance of another device, it is necessary to establish a routing path via intermediate devices. Routing protocols are important mechanism for wireless networks to establish and maintain routing paths among wireless devices by broadcasting routing messages.
To explore wireless networks, formalisms are proposed as feasible and suitable methods to specify and verify communication features of such systems. The main motivation of this paper is to explore the formalisms on the wireless networks. We focus on communication features of wireless networks including the interactions among wireless devices as well as routing protocols used in wireless networks.
The interactions among wireless devices provide the basic communication func-tion in wireless networks. We consider the physical aspects of broadcasting com-munication including location, transmission range and communication frequency. Communication based process algebras are common approaches to formalising the low level interactions behaviours among wireless devices. We extend the Calculus of Wireless Systems by introducing the concept of guarded choice. On the basis of Unifying Theories of Programming, we propose the algebraic semantics and the denotational semantics of the calculus. We present a set of algebraic laws for the cal-culus and investigate the derivation strategy for deriving the operational semantics from the algebraic semantics.
Routing protocol of wireless networks transfers information in the network via communication function of wireless devices. According to the features when rout-ing protocol establishes and maintains routes, we focus on the protocol mechanism about the route information. Hence, we use formal specification language to specify, analyse and verify the AODV routing protocol. We abstract the interactions among wireless devices as the effects of assignments on variables. Under this high level ab-straction of communication, we can analyze the essential characteristics of routing protocol in wireless networks directly.
The main contribution of this paper includes:
●We propose the algebraic semantics of the Calculus of Wireless Systems. A set of parallel expansion laws is provided and the head normal form is pre-sented. Based on the head normal form, the derivation strategy for deriving the operational semantics from the algebraic semantics is defined. The equiv-alence between the derivation strategy and the derived operational semantics is proved, which shows the soundness and the completeness of the operational semantics from the viewpoint of the algebraic semantics. We also mechanized the linking between the algebraic semantics and the operational semantics by using rewriting logic in Maude. We also propose the denotational semantic-s for this calculus by introducing the concepts of execution state and trace to describe the behaviour of wireless networks. Based on the denotational semantics, we prove some algebra laws of wireless networks.
●We formalise the AODV routing protocol used in wireless network by for-mal specification language Z and prove properties of this protocol uising Re-ly/Guarantee method. Formal description language is used to reduce the am-biguous in protocol description documents. The interaction among devices is modelled as effects of assignments on variables. We rewrite the model speci-fied by Z into a revised version of model based on shared variable concurrent programs. Based on the revised model specified by shared variable concur-rent program, the loop freedom property and other properties of the routing protocol are verified by using the Rely/Guarantee rules.
无线网络节点设备通常是以无线电波为载体进行广播式的信息发送,这种无线网络的广播信息发送模式与传统的有线以太网络中的全局广播信息发送模式有所不同。在无线网络中,信息数据的广播发送是局部的,也就是说每个无线节点所发送的信息的传输范围是有限的,只有那些处于节点传输半径覆盖范围内的部分接收节点才能够接收到所对应的节点广播发送的信息。受限于有限的信息传输范围,为了使得不在传输范围内的两个无线节点之间能够实现交互,就需要借助其他的中间节点来建立起一条能够传输信息的路由路径。路由协议是实现无线网络中路由路径的建立和维护的一种重要机制,主要是通过各种报文信息在无线网络中的广播来建立路由路径。
形式化方法被认为是对无线网络系统进行描述和验证的一种可行并且合适的方式。本文研究面向无线网络系统的形式化方法。我们主要研究无线网络中与通信交互相关的无线网络特性,包括无线节点之间的广播通信交互行为以及无线网络中路由协议建立路由路径的机制。
无线网络中无线节点之间的通信实现了无线网路中最根本的信息交互功能。我们考虑无线广播通信的各种物理特征,包括了无线节点的位置、通信范围、通信频率等物理因素。针对通信交互等无线节点底层物理行为的形式化描述和建模通常采用基于通信交互的进程代数演算系统。因此,我们扩展无线系统演算引入无线网络卫兵选择的概念,基于程序统一理提出了无线演算系统的代数语义和指称语义。我们给出了一系列无线系统演算的代数规则,研究从代数语义计算推导出操作语义的方法。
无线网络中的路由协议借助无线节点之间的通信交互实现了无线网络中的全局信息交互。针对无线网络中路由协议在路由建立和维护路由路径时的特点,我们主要考虑路由协议实现路由时的各种路由信息数据的处理机制。因此我们采用形式化描述语言对无线网络AODV路由协议进行形式化建模、分析和验证工作并且将底层的无线节点的通信交互行为抽象为针对变量的赋值效果。通过使用这种在更高层次的抽象描述方式,我们能够更直接地分析无线网络路由协议的本质特性。
本文的主要贡献包括：
·我们提出了无线系统演算的代数语义,给出了一组用于描述无线系统演算并行组合线性展开的代数规则,并且定义了无线网络系统的规范型。借助无线网络系统的规范型,我们给出了从代数语义计算生成操作语义的方法,并且证明了代数语义和操作语义的一致性,从代数语义的角度保证了操作语义的正确性和完备性。我们使用重写逻辑工具Maude实现了从代数语义自动计算操作语义的过程。我们提出了无线系统演算的指称语义,引入了无线网络执行状态和执行轨迹的概念用来描述无线网络的行为。基于指称语义模型,我们证明了无线网络系统的代数性质。
·我们使用形式化建模语言Z对无线网络中使用的AODV路由协议进行建模,并且使用基于Rely/Guarantee方法的形式化验证技术证明了协议的性质。通过形式化建模语言,我们在建模过程中消除了路由协议相关文档中自然语言描述的二义性。我们使用程序变量赋值的效果来描述无线节点之间的通信交互。我们对使用形式化语言Z构建的协议模型进行重写得到基于共享变量并行程序语言的改进协议模型。以共享变量并行程序所描述的路由协议形式化模型为基础,我们使用Rely/Guarantee推理规则证明了路由协议建立的路由路径不存在路由环路等性质。
Wireless networks have become prevalent relatively recently in our daily life. Wireless networks and applications are suitable solutions and being deployed in a wide range of communication scenarios, especially in infrastructurcless situations. Wireless devices are the basic components of wireless networks, which provide basic functions of communication and implement applications in wireless networks.
Wireless devices communicate with each other by broadcasting messages, which is quite different from the more conventional wired-based broadcast in Ethernet systems. Broadcast in wireless networks is local, i.e., a transmission covers a limited range and only a subset of all the devices in the network can receive the broadcasted message. Due to the limited transmission range of wireless devices, two remote wireless devices cannot communicate with each other directly. In order to transfer messages to a wireless device from a distance of another device, it is necessary to establish a routing path via intermediate devices. Routing protocols are important mechanism for wireless networks to establish and maintain routing paths among wireless devices by broadcasting routing messages.
To explore wireless networks, formalisms are proposed as feasible and suitable methods to specify and verify communication features of such systems. The main motivation of this paper is to explore the formalisms on the wireless networks. We focus on communication features of wireless networks including the interactions among wireless devices as well as routing protocols used in wireless networks.
The interactions among wireless devices provide the basic communication func-tion in wireless networks. We consider the physical aspects of broadcasting com-munication including location, transmission range and communication frequency. Communication based process algebras are common approaches to formalising the low level interactions behaviours among wireless devices. We extend the Calculus of Wireless Systems by introducing the concept of guarded choice. On the basis of Unifying Theories of Programming, we propose the algebraic semantics and the denotational semantics of the calculus. We present a set of algebraic laws for the cal-culus and investigate the derivation strategy for deriving the operational semantics from the algebraic semantics.
Routing protocol of wireless networks transfers information in the network via communication function of wireless devices. According to the features when rout-ing protocol establishes and maintains routes, we focus on the protocol mechanism about the route information. Hence, we use formal specification language to specify, analyse and verify the AODV routing protocol. We abstract the interactions among wireless devices as the effects of assignments on variables. Under this high level ab-straction of communication, we can analyze the essential characteristics of routing protocol in wireless networks directly.
The main contribution of this paper includes:
●We propose the algebraic semantics of the Calculus of Wireless Systems. A set of parallel expansion laws is provided and the head normal form is pre-sented. Based on the head normal form, the derivation strategy for deriving the operational semantics from the algebraic semantics is defined. The equiv-alence between the derivation strategy and the derived operational semantics is proved, which shows the soundness and the completeness of the operational semantics from the viewpoint of the algebraic semantics. We also mechanized the linking between the algebraic semantics and the operational semantics by using rewriting logic in Maude. We also propose the denotational semantic-s for this calculus by introducing the concepts of execution state and trace to describe the behaviour of wireless networks. Based on the denotational semantics, we prove some algebra laws of wireless networks.
●We formalise the AODV routing protocol used in wireless network by for-mal specification language Z and prove properties of this protocol uising Re-ly/Guarantee method. Formal description language is used to reduce the am-biguous in protocol description documents. The interaction among devices is modelled as effects of assignments on variables. We rewrite the model speci-fied by Z into a revised version of model based on shared variable concurrent programs. Based on the revised model specified by shared variable concur-rent program, the loop freedom property and other properties of the routing protocol are verified by using the Rely/Guarantee rules.
引文
[1]Jean-Raymond Abrial. Data semantics. In IFIP Working Conference Data Base Management, pages 1-60,1974.
[2]Krzysztof R. Apt. Ten Years of Hoare's Logic:A Survey-Part Ⅰ. ACM Trans. Program. Lang. Syst.,3(4):431-483,1981.
[3]Krzysztof R. Apt. Ten Years of Hoare's Logic:A Survey-Part Ⅱ:Nondeter-minism. Theor. Comput. Sci.,28:83-109,1984.
[4]Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press,2008.
[5]Jan A. Bergstra and Jan Willem Klop. Algebra of communicating processes with abstraction. Theor. Comput. Sci.,37:77-121,1985.
[6]Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor O-bradovic, Oleg Sokolsky, and Mahesh Viswanathan. Verisim:Formal analysis of network simulations. In ISSTA 2000, pages 2-13,2000.
[7]Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor O-bradovic, Oleg Sokolsky, and Mahesh Viswanathan. Verisim:Formal analysis of network simulations. IEEE Trans. Software Eng.,28(2):129-145,2002.
[8]Azzedine Boukerche, Begumhan Turgut, Nevin Aydin, Mohammad Z. Ahmad, Ladislau Boloni, and Damla Turgut. Routing protocols in ad hoc networks: A survey. Computer Networks,55(13):3032-3080,2011.
[9]Jonathan P. Bowen. Formal Specification and Documentation using Z:A Case Study Approach. International Thomson Computer Press,2003.
[10]Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers,35(8):677-691,1986.
[11]Tracy Camp, Jeff Boleng, and Vanessa Davies. A survey of mobility models for ad hoc network research. Wireless Communications and Mobile Computing, 2(5):483-502,2002.
[12]Ana Cavalcanti, Andy J. Wellings, and Jim Woodcock. The Safety-Critical Java memory model formalised. Formal Asp. Comput.,25(1):37-57,2013.
[13]Andrea Cerone and Matthew Hennessy. Modelling probabilistic wireless net-works. Logical Methods in Computer Science,9(3),2013.
[14]Ioannis Chatzigiannakis, Tassos Dimitriou, Marios Mavronicolas, Sotiris E. Nikoletseas, and Paul G. Spirakis. A comparative study of protocols for effi-cient data propagation in smart dust networks. Parallel Processing Letters, 13(4):615-627,2003.
[15]Sibusisiwe Chiyangwa and Marta Z. Kwiatkowska. A timing analysis of aodv. In FMOODS 2005:Formal Methods for Open Object-Based Distributed Sys-tems,7th IFIP WG 6.1 International Conference, Athens, Greece, June 15-17, 2005, Proceedings, volume 3535 of Lecture Notes in Computer Science, pages 306-321. Springer,2005.
[16]Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press,1999.
[17]Manuel Clavel, Francisco Duran, Steven Eker, Patrick Lincoln, Narciso Marti-Oliet, Jose Meseguer, and Jose F. Quesada. Maude:specification and pro-gramming in rewriting logic. Theor. Comput. Sci.,285(2)-.187-243,2002.
[18]Manuel Clavel, Francisco Duran, Steven Eker, Patrick Lincoln, Narciso Marti-Oliet, Jose Meseguer, and Carolyn Talcott. All About Maude-a High-performance Logical Framework:How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Vcrlag, Berlin, Heidelberg,2007.
[19]Satyaki Das and David L. Dill. Counter-example based predicate discovery in predicate abstraction. In FMCAD 2002:Formal Methods in Computer-Aided Design,4th International Conference, Portland, OR, USA, November 6-8,2002, volume 2517 of Lecture Notes in Computer Science, pages 19-32. Springer,2002.
[20]John Derrick and Eerke Boiten. Refmement in Z and Object-Z. Springer-Vcrlag,2nd edition,2014.
[21]Josee Desharnais, Vineet Gupta, Radha Jagadcesan, and Prakash Panan-gaden. Metrics for labelled markov processes. Theor. Comput. Sci., 318(3):323-354,2004.
[22]Edsger W. Dijkstra. Guarded commands, non-detcrminancy and a calculus for the derivation of programs. In Language Hierarchies and Interfaces, Inter-national Summer School, Marktoberdorf, Germany, July 23-August 2,1975, volume 46 of Lecture Notes in Computer Science, pages 111-124. Springer, 1975.
[23]David A. Duffy. Principles of Automated Theorem Proving. John Wiley & Sons, Inc.,1991.
[24]Roger Duke and Gordon Rose. Formal Object Oriented Specification Using Objcct-Z. Palgravc Macmillan,2000.
[25]Dawson R. Engler and Madanlal Musuvathi. Static analysis versus software model checking for bug finding. In VMCAI 2004:Verification, Model Check-ing, and Abstract Interpretation,5th International Conference, Venice, Jan-uary 11-13,2004, volume 2937 of Lecture Notes in Computer Science, pages 191-210. Springer,2004.
[26]Ansgar Fehnker, Rob J. van Glabbcek, Peter Hofner, Annabcllc McIvcr, Mar-ius Portmann, and Wee Lum Tan. A process algebra for wireless mesh net-works. In ESOP 2012:Programming Languages and Systems-21st European Symposium on Programming, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 April 1,2012, volume 7211 of Lecture Notes in Computer Science, pages 295-315. Springer,2012.
[27]Ansgar Fchnkcr, Rob J. van Glabbcck, Peter Hofncr, Annabcllc McIver, Mar-ius Portmann, and Wee Lum Tan. A process algebra for wireless mesh networks used for modelling, verifying and analysing aodv. In Tech. Rep.5513, NICTA, 2012,2012.
[28]Matthias Fellcisen and Robert Hicb. The revised report on the syntactic theories of sequential control and state. Thcor. Cornput. Sci.,103(2):235-271,1992.
[29]R. W. Floyd. Assigning meanings to programs. Proceedings of the Amcricatn Mathematical Society Symposia on Applied Mathematics,19:19-31,1967.
[30]Fatemch Ghassemi, Wan Fokkink, and Ali Movaghar. Restricted broadcast process theory. In SEFM 2008:6th IEEE International Conference on Software Engineering and Formal Methods, Cape Town, South Africa,10-14 November,2008, pages 345-354. IEEE Computer Society,2008.
[31]Jens Chr. Godskcsen. A calculus for mobile ad hoc networks. In COORDI-NATION 2007, volume 4467, pages 132-150,2007.
[32]Andrea Goldsmith. Wireless Communications. Cambridge University Press, New York, NY, USA,2005.
[33]I. Hayes. Specification Case Studies. Prentice-Hall,2nd edition,1993.
[34]Jifcng He, Zhiming Liu, Xiaoshan Li, and Shcngchao Qin. A relational model for object-oriented designs. In APLAS 2004:Programming Languages and Systems:Second Asian Symposium, Taipei, Taiwan, November 4-6,2004, volume 3302 of Lecture Notes in Computer Science, pages 415-436. Springer, 2004.
[35]Jifeng He, Karen Seidcl, and Annabcllc McIvcr. Probabilistic models for the guarded command language. Sci. Comput. Program.,28(2-3):171-192,1997.
[36]M. Hcnncssy. The Semantics of Programming Language:An Elementary Introduction using Structural Operational Semantics. John Wiley & Sons, 1990.
[37]C. A. R Hoare. An axiomatic basis for computer programming. Communica-tions of the ACM,12(10):576-580,1969.
[38]C. A. R Hoare. Communicating sequential processes. Communication of the ACM,21(8):666-677,1978.
[39]C. A. R Hoare. Communicating Sequential Processes. Prentice Hall Interna-tional Series in Computer Science,1985.
[40]C. A. R. Hoare, Ian J. Hayes. Jifeng He, Carroll Morgan, A. W. Roscoe, Jeff W. Sanders, Ib Holm S(?)rensen, J. Michael Spivey, and Bernard Sufrin. Laws of programming. Commun. ACM,30(8):672-686,1987.
[41]C. A. R. Hoare and Jifcng He. Unifying Theories of Programming. Prentice Hall International Series in Computer Science,1998.
[42]Daniel Jackson. Alloy:A lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol., 11(2):256-290, April 2002.
[43]Daniel Jackson. Software Abstractions:Logic, Language, and Analysis. The MIT Press,2006.
[44]Cliff B. Jones. Development Methods for Computer Programs including a No-tation of Interference. Phd thesis, Oxford University Computing Laboratory, 1981.
[45]Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst.,5(4):596-619,1983.
[46]Computer Science Laboratory. The Maude System. Department of Comput-er Science, University of Illinois at Urbana-Champaign. http://maude. cs. uiuc. edu.
[47]Ivan Lanese and Davide Sangiorgi. An operational semantics for a calculus for wireless systems. Theor. Comput. Sci.,411(19):1928-1948,2010.
[48]Kevin Lano. Z++, an object-orientated extension to z. In Z User Workshop, Workshops in Computing, pages 151-172. Springer,1990.
[49]Luciano Lavagno, Grant Martin, and Louis Scheffer. Electronic Design Au-tomation for Integrated Circuits Handbook-2 Volume Set. CRC Press, Inc., 2006.
[50]Xiaoshan Li, Zhiming Liu, and Jifeng He. A formal semantics of uml sequence diagram. In ASWEC 2004:15th Australian Software Engineering Conference, 13-16 April 2004, Melbourne, Australia, pages 168-177. IEEE Computer So-ciety,2004.
[51]Zhiming Liu, Jifcng He, Xiaoshan Li, and Yifcng Chen. A relational model for formal object-oriented requirement analysis in uml. In ICFEM 2003: 5th International Conference on Formal Engineering Methods November 5-7, 2003, Singapore, volume 2885 of Lecture Notes in Computer Science, pages 641-664. Springer,2003.
[52]Donald W. Loveland. Automated Theorem Proving:A Logical Basis (Fun-damental Studies in Computer Science). Elsevier North-Holland,1978.
[53]Narciso Marti-Oliet and Jose Meseguer. Rewriting logic as a logical and se-mantic framework. Elcctr. Notes Theor. Comput. Sci.,4:190-225,1996.
[54]Theodore McCombs. Maude 2.0 Primer (Version 1.0). Technical report, Com-puter Science Laboratory, Department of Computer Science, University of Illinois at Urbana-Champaign,2003.
[55]A. McIver and C. Morgan. Abstraction, Refinement and Proof of Probability Systems. Monographs in Computer Science. Springer,2004.
[56]Massimo Merro. An observational theory for mobile ad hoc networks (full version). Inf. Comput.,207(2):194-208,2009.
[57]Massimo Merro, Francesco Ballardin, and Elconora Sibilio. A timed calculus for wireless systems.412(47):6585-6611,2011.
[58]Nicola Mezzetti and Davide Sangiorgi. Towards a calculus for wireless systems, volume 158, pages 331-353,2006.
[59]R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer,1980.
[60]R. Milner. Communication and Concurrency. Prentice Hall International Series in Computer Science,1990.
[61]R. Milner. The polyadic π-calculus:A tutorial. Technical Report ECS-LFCS-91-190, Edinburgh University,1991.
[62]R. Milner. Communication and Mobile System:π-calculus. Cambridge Uni-versity Press,1999.
[63]Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile pro-cesses, (parts I and II). In Information and Computation, volume 100, pages 1-77,1992.
[64]Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Englcr, and David L. Dill. Cmc:A pragmatic approach to model checking real code. In OSDI 2002:5th Symposium on Operating System Design and Implementa-tion, Boston, Massachusetts, USA, December 9-11,2002. USENIX Associa-tion,2002.
[65]Sebastian Nanz and Chris Hankin. Formal security analysis for ad-hoc net-works. Elcctr. Notes Thcor. Comput. Sci.,142:195-213,2006.
[66]Sotiris E. Nikolctscas. Models and algorithms for wireless sensor networks (smart dust). In SOFSEM 2006:32nd Conference on Current Trends in Theory and Practice of Computer Science, Merin, Czech Republic, January 21-27,2006, volume 3831 of Lecture Notes in Computer Science, pages 64-83. Springer,2006.
[67]Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. Formal development of industrial-scale systems in circus. ISSE,1(2):125-146,2005.
[68]Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. A denotational seman-tics for circus. Elcctr. Notes Thcor. Comput. Sci.,187:107-123,2007.
[69]Peter Csaba Olveczky and Jose Meseguer. Specification and analysis of real-time systems using real-time maudc. In FASE 2004:7th International Con-ference on Fundamental Approaches to Software Engineering, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29-april 2,2004, volume 2984 of Lecture Notes in Computer Science, pages 354-358. Springer,2004.
[70]Peter Csaba Olveozky and Jose Meseguer. Semantics and pragmatics of real-time maude. Higher-Order and Symbolic Computation,20(1-2):161-196, 2007.
[71]Karol Ostrovsky, K. V. S. Prasad, and Walid Taha.4th international acm sigplan conference on principles and practice of declarative programming, oc-tober 6-8,2002, Pittsburgh, pa, usa (affiliated with pli 2002). In Towards a primitive higher order calculus of broadcasting systems, pages 2-13. ACM, 2002.
[72]Susan S. Owicki and David Gries. An axiomatic proof technique for parallel programs i. Acta Inf.,6:319-340,1976.
[73]Kavch Pahlavan and Prashant Krishnamurthy. Principles of Wireless Net-works:A Unified Approach. Prentice Hall PTR, Upper Saddle River, NJ, USA,1st edition,2001.
[74]Kavch Pahlavan and Allen H. Levesque. Wireless Information Networks. Wiley-Interscience, New York, NY, USA,1995.
[75]Charles E. Perkins and Elizabeth M. Bclding-Roycr. Ad-hoc On-Demand Dis-tance Vector Routing. In WMCSA'99:2nd Workshop on Mobile Computing Systems and Applications, February 25-26,1999, New Orleans, LA, USA, pages 90-100. IEEE Computer Society,1999.
[76]Charles E. Perkins, Elizabeth M. Belding-Royer, and Samir Das. Ad hoc on-demand distance vector (AODV) routing (RFC Editor).2004.
[77]Gordon Plotkin. A powcrdomain construction. SIAM Journal on Computing, 1976.
[78]Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algcbr. Program,60-61:17-139,2004.
[79]K. V. S. Prasad. A calculus of broadcasting systems. Sci. Comput. Program. 25(2-3):285-327,1995.
[80]K. V. S. Prasad. Broadcasting in time. In COORDINATION'96, Cescna, Italy, April 15-17,1996, volume 1061 of Lecture Notes in Computer Science, pages 321-338. Springer,1996.
[81]Community Z Tools Project. CZT:Community Z Tools. Tools for developing and reasoning about Z specifications, http://czt.sourceforge.net.
[82]Shcngchao Qin, Jifcng He, Zongyan Qiu, and Naixiao Zhang. An alge-braic hardware/software partitioning algorithm. J. Comput. Sci. Technol. 17(3):284-294,2002.
[83]Theodore Rappaport. Wireless Communications:Principles and Practice. Prentice Hall PTR, Upper Saddle River, NJ, USA,2nd edition,2001.
[84]A. W. Roscoe and C. A. R. Hoare. The laws of occam programming. Theor. Comput. Sci.,60:177-229,1988.
[85]A. W. Roscoe, C. A. R. Hoare, and Richard Bird. The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River, NJ, USA,1997.
[86]D. A. Schmidt. Denotational Semantics:A Methodology for Language De-velopment. Allyn and Bacon,1986.
[87]D. Scott and C. Strachey. Towards a mathematical semantics for computer language. Technical Report PRG-6, Oxford University Computer Laboratory, 1971.
[88]Anu Singh, C. R. Ramakrishnan, and Scott A. Smolka. A process calculus for mobile ad hoc networks.75(6):440-469,2010.
[89]Graeme Smith. The Object-Z Specification Language. Kluwer Academic Publishers, Norwell, MA, USA,2000.
[90]Michael Smyth. Power domains. Journal of Computer and System Sciences, 1978.
[91]J.M. Spivey. The Z Notation:A Reference Manual. Prentice-Hall,2nd edition, 1992.
[92]J. Stoy. Denotaional Semantics:The Scott-Strachey Approach to Program-ming Language. MIT Press,1977.
[93]C. Strachey. Towards a formal semantics. In Formal Language Description Languages for Computer Programming. Proceedings of the IFIP Working Con-ference, Vienna, pages 197-220,1966.
[94]Bharath Sundararaman, Ugo Buy, and Ajay D. Kshemkalyani. Clock synchro-nization for wireless sensor networks:A survey. Ad Hoc Networks (Elsevier, 3:281-323,2005.
[95]Xinbci Tang and Jim Woodcock. Towards mobile processes in unifying theo-ries. In SEFM 2004:2nd International Conference on Software Engineering and Formal Methods, Beijing, China, September 26-30,2004, pages 44-53. IEEE Computer Society,2004.
[96]Xinbei Tang and Jim Woodcock. Travelling processes. In MPC 2004:7th International Conference on Mathematics of Program Construction, Stirling, Scotland, UK, July 12-14,2004, volume 3125 of Lecture Notes in Computer Science, pages 381-399. Springer-Verlag,2004.
[97]A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics,5:285-309,1955.
[98]Brett Warneke, Matt Last, Brian Liebowitz, and Kristofer S. J. Pister. Smart dust:Communicating with a cubic-millimeter computer. IEEE Computer, 34(1):44-51,2001.
[99]D. Watt. Programming Language Syntax and Semantics. Prentice Hall,1991.
[100]J. Woodcock and J. Davies. Using Z:Specification, Refinement, and Proof. Prcnticc-Hall,1996.
[101]Jim Woodcock and Ana Cavalcanti. The semantics of circus. In ZB 2002:2nd International Conference of B and Z Users, Grenoble, France, January 23-25, 2002, volume 2272 of Lecture Notes in Computer Science, pages 184-203. Springer,2002.
[102]Qiwen Xu, Willem P. de Rocvcr, and Jifeng He. The rely-guarantcc method for verifying shared variable concurrent programs. Formal Asp. Comput. 9(2):149-174,1997.
[103]Ming Zhou, Huabing Yang, Xingyuan Zhang, and Jinshuang Wang. The proof of aodv loop freedom. In WCSP 2009:International Conference on Wireless Communications Signal Processing, pages 1-5, Nov 2009.
[104]Huibiao Zhu, Jonathan P. Bowcn, and Jifcng He. Deriving operational seman-tics from denotational semantics for verilog. In APSEC 2001:8th Asia-Pacific Software Engineering Conference,4-7 December 2001, Macau, China, pages 177-184. IEEE Computer Society,2001.
[105]Huibiao Zhu, Jonathan P. Bowen, and Jifeng He. From operational semantics to denotational semantics for verilog. In CHARME 2001:11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Livingston, Scotland, UK, September 4-7,2001, volume 2144 of Lecture Notes in Computer Science, pages 449-466. Springer, 2001.
[106]Huibiao Zhu, Jonathan P. Bowen, and Jifeng He. Soundness, completeness and non-redundancy of operational semantics for verilog based on denota-tional semantics. In ICFEM 2002:4th International Conference on Formal Engineering Methods, Shanghai, China, October 21-25,2002, volume 2495 of Lecture Notes in Computer Science, pages 600-612. Springer,2002.
[107]Huibiao Zhu, Jifeng He, and Jonathan P. Bowen. From algebraic semantics to denotational semantics for verilog. In ICECCS 2006:11th International Conference on Engineering of Complex Computer Systems,15-17 August 2006, Stanford, California, USA, pages 139-151. IEEE Computer Society,2006.
[108]Huibiao Zhu, Jifeng He, and Jonathan P. Bowen. From algebraic semantics to denotational semantics for verilog. ISSE,4(4):341-360,2008.
[109]Huibiao Zhu, Jifeng He, and Jing Li. Unifying denotational semantics with operational semantics for web services. In ICDCIT 2007:4th International Conference on Distributed Computing and Internet Technology, Bangalore, India, December 17-20, volume 4882 of Lecture Notes in Computer Science, pages 225-239. Springer,2007.
[110]Huibiao Zhu, Jifcng He, Jing Li, and Jonathan P. Bowen. Algebraic approach to linking the semantics of web services. In SEFM 2007:5th IEEE Internation-al Conference on Software Engineering and Formal Methods,10-14 September 2007, London, England, UK, pages 315-328. IEEE Computer Society,2007.
[111]Huibiao Zhu, Jifeng He, Jing Li, and Jonathan P. Bowen. Algebraic approach to linking the semantics of web services. ISSE,7(3):209-224,2011.
[112]Huibiao Zhu, Jifcng He, Jing Li, Geguang Pu, and Jonathan P. Bowen. Linking denotational semantics with operational semantics for web services. ISSE, 6(4):283-298,2010.
[113]Huibiao Zhu, Gcguang Pu, and Jifeng He. A denotational approach to scope-based compensable flow language for web service. In ASIAN 2006:11th Asian Computing Science Conference, Tokyo, Japan, December 6-8,2006, volume 4435 of Lecture Notes in Computer Science, pages 28-36. Springer,2006.
[2]Krzysztof R. Apt. Ten Years of Hoare's Logic:A Survey-Part Ⅰ. ACM Trans. Program. Lang. Syst.,3(4):431-483,1981.
[3]Krzysztof R. Apt. Ten Years of Hoare's Logic:A Survey-Part Ⅱ:Nondeter-minism. Theor. Comput. Sci.,28:83-109,1984.
[4]Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press,2008.
[5]Jan A. Bergstra and Jan Willem Klop. Algebra of communicating processes with abstraction. Theor. Comput. Sci.,37:77-121,1985.
[6]Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor O-bradovic, Oleg Sokolsky, and Mahesh Viswanathan. Verisim:Formal analysis of network simulations. In ISSTA 2000, pages 2-13,2000.
[7]Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor O-bradovic, Oleg Sokolsky, and Mahesh Viswanathan. Verisim:Formal analysis of network simulations. IEEE Trans. Software Eng.,28(2):129-145,2002.
[8]Azzedine Boukerche, Begumhan Turgut, Nevin Aydin, Mohammad Z. Ahmad, Ladislau Boloni, and Damla Turgut. Routing protocols in ad hoc networks: A survey. Computer Networks,55(13):3032-3080,2011.
[9]Jonathan P. Bowen. Formal Specification and Documentation using Z:A Case Study Approach. International Thomson Computer Press,2003.
[10]Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers,35(8):677-691,1986.
[11]Tracy Camp, Jeff Boleng, and Vanessa Davies. A survey of mobility models for ad hoc network research. Wireless Communications and Mobile Computing, 2(5):483-502,2002.
[12]Ana Cavalcanti, Andy J. Wellings, and Jim Woodcock. The Safety-Critical Java memory model formalised. Formal Asp. Comput.,25(1):37-57,2013.
[13]Andrea Cerone and Matthew Hennessy. Modelling probabilistic wireless net-works. Logical Methods in Computer Science,9(3),2013.
[14]Ioannis Chatzigiannakis, Tassos Dimitriou, Marios Mavronicolas, Sotiris E. Nikoletseas, and Paul G. Spirakis. A comparative study of protocols for effi-cient data propagation in smart dust networks. Parallel Processing Letters, 13(4):615-627,2003.
[15]Sibusisiwe Chiyangwa and Marta Z. Kwiatkowska. A timing analysis of aodv. In FMOODS 2005:Formal Methods for Open Object-Based Distributed Sys-tems,7th IFIP WG 6.1 International Conference, Athens, Greece, June 15-17, 2005, Proceedings, volume 3535 of Lecture Notes in Computer Science, pages 306-321. Springer,2005.
[16]Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press,1999.
[17]Manuel Clavel, Francisco Duran, Steven Eker, Patrick Lincoln, Narciso Marti-Oliet, Jose Meseguer, and Jose F. Quesada. Maude:specification and pro-gramming in rewriting logic. Theor. Comput. Sci.,285(2)-.187-243,2002.
[18]Manuel Clavel, Francisco Duran, Steven Eker, Patrick Lincoln, Narciso Marti-Oliet, Jose Meseguer, and Carolyn Talcott. All About Maude-a High-performance Logical Framework:How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Vcrlag, Berlin, Heidelberg,2007.
[19]Satyaki Das and David L. Dill. Counter-example based predicate discovery in predicate abstraction. In FMCAD 2002:Formal Methods in Computer-Aided Design,4th International Conference, Portland, OR, USA, November 6-8,2002, volume 2517 of Lecture Notes in Computer Science, pages 19-32. Springer,2002.
[20]John Derrick and Eerke Boiten. Refmement in Z and Object-Z. Springer-Vcrlag,2nd edition,2014.
[21]Josee Desharnais, Vineet Gupta, Radha Jagadcesan, and Prakash Panan-gaden. Metrics for labelled markov processes. Theor. Comput. Sci., 318(3):323-354,2004.
[22]Edsger W. Dijkstra. Guarded commands, non-detcrminancy and a calculus for the derivation of programs. In Language Hierarchies and Interfaces, Inter-national Summer School, Marktoberdorf, Germany, July 23-August 2,1975, volume 46 of Lecture Notes in Computer Science, pages 111-124. Springer, 1975.
[23]David A. Duffy. Principles of Automated Theorem Proving. John Wiley & Sons, Inc.,1991.
[24]Roger Duke and Gordon Rose. Formal Object Oriented Specification Using Objcct-Z. Palgravc Macmillan,2000.
[25]Dawson R. Engler and Madanlal Musuvathi. Static analysis versus software model checking for bug finding. In VMCAI 2004:Verification, Model Check-ing, and Abstract Interpretation,5th International Conference, Venice, Jan-uary 11-13,2004, volume 2937 of Lecture Notes in Computer Science, pages 191-210. Springer,2004.
[26]Ansgar Fehnker, Rob J. van Glabbcek, Peter Hofner, Annabcllc McIvcr, Mar-ius Portmann, and Wee Lum Tan. A process algebra for wireless mesh net-works. In ESOP 2012:Programming Languages and Systems-21st European Symposium on Programming, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 April 1,2012, volume 7211 of Lecture Notes in Computer Science, pages 295-315. Springer,2012.
[27]Ansgar Fchnkcr, Rob J. van Glabbcck, Peter Hofncr, Annabcllc McIver, Mar-ius Portmann, and Wee Lum Tan. A process algebra for wireless mesh networks used for modelling, verifying and analysing aodv. In Tech. Rep.5513, NICTA, 2012,2012.
[28]Matthias Fellcisen and Robert Hicb. The revised report on the syntactic theories of sequential control and state. Thcor. Cornput. Sci.,103(2):235-271,1992.
[29]R. W. Floyd. Assigning meanings to programs. Proceedings of the Amcricatn Mathematical Society Symposia on Applied Mathematics,19:19-31,1967.
[30]Fatemch Ghassemi, Wan Fokkink, and Ali Movaghar. Restricted broadcast process theory. In SEFM 2008:6th IEEE International Conference on Software Engineering and Formal Methods, Cape Town, South Africa,10-14 November,2008, pages 345-354. IEEE Computer Society,2008.
[31]Jens Chr. Godskcsen. A calculus for mobile ad hoc networks. In COORDI-NATION 2007, volume 4467, pages 132-150,2007.
[32]Andrea Goldsmith. Wireless Communications. Cambridge University Press, New York, NY, USA,2005.
[33]I. Hayes. Specification Case Studies. Prentice-Hall,2nd edition,1993.
[34]Jifcng He, Zhiming Liu, Xiaoshan Li, and Shcngchao Qin. A relational model for object-oriented designs. In APLAS 2004:Programming Languages and Systems:Second Asian Symposium, Taipei, Taiwan, November 4-6,2004, volume 3302 of Lecture Notes in Computer Science, pages 415-436. Springer, 2004.
[35]Jifeng He, Karen Seidcl, and Annabcllc McIvcr. Probabilistic models for the guarded command language. Sci. Comput. Program.,28(2-3):171-192,1997.
[36]M. Hcnncssy. The Semantics of Programming Language:An Elementary Introduction using Structural Operational Semantics. John Wiley & Sons, 1990.
[37]C. A. R Hoare. An axiomatic basis for computer programming. Communica-tions of the ACM,12(10):576-580,1969.
[38]C. A. R Hoare. Communicating sequential processes. Communication of the ACM,21(8):666-677,1978.
[39]C. A. R Hoare. Communicating Sequential Processes. Prentice Hall Interna-tional Series in Computer Science,1985.
[40]C. A. R. Hoare, Ian J. Hayes. Jifeng He, Carroll Morgan, A. W. Roscoe, Jeff W. Sanders, Ib Holm S(?)rensen, J. Michael Spivey, and Bernard Sufrin. Laws of programming. Commun. ACM,30(8):672-686,1987.
[41]C. A. R. Hoare and Jifcng He. Unifying Theories of Programming. Prentice Hall International Series in Computer Science,1998.
[42]Daniel Jackson. Alloy:A lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol., 11(2):256-290, April 2002.
[43]Daniel Jackson. Software Abstractions:Logic, Language, and Analysis. The MIT Press,2006.
[44]Cliff B. Jones. Development Methods for Computer Programs including a No-tation of Interference. Phd thesis, Oxford University Computing Laboratory, 1981.
[45]Cliff B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst.,5(4):596-619,1983.
[46]Computer Science Laboratory. The Maude System. Department of Comput-er Science, University of Illinois at Urbana-Champaign. http://maude. cs. uiuc. edu.
[47]Ivan Lanese and Davide Sangiorgi. An operational semantics for a calculus for wireless systems. Theor. Comput. Sci.,411(19):1928-1948,2010.
[48]Kevin Lano. Z++, an object-orientated extension to z. In Z User Workshop, Workshops in Computing, pages 151-172. Springer,1990.
[49]Luciano Lavagno, Grant Martin, and Louis Scheffer. Electronic Design Au-tomation for Integrated Circuits Handbook-2 Volume Set. CRC Press, Inc., 2006.
[50]Xiaoshan Li, Zhiming Liu, and Jifeng He. A formal semantics of uml sequence diagram. In ASWEC 2004:15th Australian Software Engineering Conference, 13-16 April 2004, Melbourne, Australia, pages 168-177. IEEE Computer So-ciety,2004.
[51]Zhiming Liu, Jifcng He, Xiaoshan Li, and Yifcng Chen. A relational model for formal object-oriented requirement analysis in uml. In ICFEM 2003: 5th International Conference on Formal Engineering Methods November 5-7, 2003, Singapore, volume 2885 of Lecture Notes in Computer Science, pages 641-664. Springer,2003.
[52]Donald W. Loveland. Automated Theorem Proving:A Logical Basis (Fun-damental Studies in Computer Science). Elsevier North-Holland,1978.
[53]Narciso Marti-Oliet and Jose Meseguer. Rewriting logic as a logical and se-mantic framework. Elcctr. Notes Theor. Comput. Sci.,4:190-225,1996.
[54]Theodore McCombs. Maude 2.0 Primer (Version 1.0). Technical report, Com-puter Science Laboratory, Department of Computer Science, University of Illinois at Urbana-Champaign,2003.
[55]A. McIver and C. Morgan. Abstraction, Refinement and Proof of Probability Systems. Monographs in Computer Science. Springer,2004.
[56]Massimo Merro. An observational theory for mobile ad hoc networks (full version). Inf. Comput.,207(2):194-208,2009.
[57]Massimo Merro, Francesco Ballardin, and Elconora Sibilio. A timed calculus for wireless systems.412(47):6585-6611,2011.
[58]Nicola Mezzetti and Davide Sangiorgi. Towards a calculus for wireless systems, volume 158, pages 331-353,2006.
[59]R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer,1980.
[60]R. Milner. Communication and Concurrency. Prentice Hall International Series in Computer Science,1990.
[61]R. Milner. The polyadic π-calculus:A tutorial. Technical Report ECS-LFCS-91-190, Edinburgh University,1991.
[62]R. Milner. Communication and Mobile System:π-calculus. Cambridge Uni-versity Press,1999.
[63]Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile pro-cesses, (parts I and II). In Information and Computation, volume 100, pages 1-77,1992.
[64]Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Englcr, and David L. Dill. Cmc:A pragmatic approach to model checking real code. In OSDI 2002:5th Symposium on Operating System Design and Implementa-tion, Boston, Massachusetts, USA, December 9-11,2002. USENIX Associa-tion,2002.
[65]Sebastian Nanz and Chris Hankin. Formal security analysis for ad-hoc net-works. Elcctr. Notes Thcor. Comput. Sci.,142:195-213,2006.
[66]Sotiris E. Nikolctscas. Models and algorithms for wireless sensor networks (smart dust). In SOFSEM 2006:32nd Conference on Current Trends in Theory and Practice of Computer Science, Merin, Czech Republic, January 21-27,2006, volume 3831 of Lecture Notes in Computer Science, pages 64-83. Springer,2006.
[67]Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. Formal development of industrial-scale systems in circus. ISSE,1(2):125-146,2005.
[68]Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. A denotational seman-tics for circus. Elcctr. Notes Thcor. Comput. Sci.,187:107-123,2007.
[69]Peter Csaba Olveczky and Jose Meseguer. Specification and analysis of real-time systems using real-time maudc. In FASE 2004:7th International Con-ference on Fundamental Approaches to Software Engineering, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29-april 2,2004, volume 2984 of Lecture Notes in Computer Science, pages 354-358. Springer,2004.
[70]Peter Csaba Olveozky and Jose Meseguer. Semantics and pragmatics of real-time maude. Higher-Order and Symbolic Computation,20(1-2):161-196, 2007.
[71]Karol Ostrovsky, K. V. S. Prasad, and Walid Taha.4th international acm sigplan conference on principles and practice of declarative programming, oc-tober 6-8,2002, Pittsburgh, pa, usa (affiliated with pli 2002). In Towards a primitive higher order calculus of broadcasting systems, pages 2-13. ACM, 2002.
[72]Susan S. Owicki and David Gries. An axiomatic proof technique for parallel programs i. Acta Inf.,6:319-340,1976.
[73]Kavch Pahlavan and Prashant Krishnamurthy. Principles of Wireless Net-works:A Unified Approach. Prentice Hall PTR, Upper Saddle River, NJ, USA,1st edition,2001.
[74]Kavch Pahlavan and Allen H. Levesque. Wireless Information Networks. Wiley-Interscience, New York, NY, USA,1995.
[75]Charles E. Perkins and Elizabeth M. Bclding-Roycr. Ad-hoc On-Demand Dis-tance Vector Routing. In WMCSA'99:2nd Workshop on Mobile Computing Systems and Applications, February 25-26,1999, New Orleans, LA, USA, pages 90-100. IEEE Computer Society,1999.
[76]Charles E. Perkins, Elizabeth M. Belding-Royer, and Samir Das. Ad hoc on-demand distance vector (AODV) routing (RFC Editor).2004.
[77]Gordon Plotkin. A powcrdomain construction. SIAM Journal on Computing, 1976.
[78]Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algcbr. Program,60-61:17-139,2004.
[79]K. V. S. Prasad. A calculus of broadcasting systems. Sci. Comput. Program. 25(2-3):285-327,1995.
[80]K. V. S. Prasad. Broadcasting in time. In COORDINATION'96, Cescna, Italy, April 15-17,1996, volume 1061 of Lecture Notes in Computer Science, pages 321-338. Springer,1996.
[81]Community Z Tools Project. CZT:Community Z Tools. Tools for developing and reasoning about Z specifications, http://czt.sourceforge.net.
[82]Shcngchao Qin, Jifcng He, Zongyan Qiu, and Naixiao Zhang. An alge-braic hardware/software partitioning algorithm. J. Comput. Sci. Technol. 17(3):284-294,2002.
[83]Theodore Rappaport. Wireless Communications:Principles and Practice. Prentice Hall PTR, Upper Saddle River, NJ, USA,2nd edition,2001.
[84]A. W. Roscoe and C. A. R. Hoare. The laws of occam programming. Theor. Comput. Sci.,60:177-229,1988.
[85]A. W. Roscoe, C. A. R. Hoare, and Richard Bird. The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River, NJ, USA,1997.
[86]D. A. Schmidt. Denotational Semantics:A Methodology for Language De-velopment. Allyn and Bacon,1986.
[87]D. Scott and C. Strachey. Towards a mathematical semantics for computer language. Technical Report PRG-6, Oxford University Computer Laboratory, 1971.
[88]Anu Singh, C. R. Ramakrishnan, and Scott A. Smolka. A process calculus for mobile ad hoc networks.75(6):440-469,2010.
[89]Graeme Smith. The Object-Z Specification Language. Kluwer Academic Publishers, Norwell, MA, USA,2000.
[90]Michael Smyth. Power domains. Journal of Computer and System Sciences, 1978.
[91]J.M. Spivey. The Z Notation:A Reference Manual. Prentice-Hall,2nd edition, 1992.
[92]J. Stoy. Denotaional Semantics:The Scott-Strachey Approach to Program-ming Language. MIT Press,1977.
[93]C. Strachey. Towards a formal semantics. In Formal Language Description Languages for Computer Programming. Proceedings of the IFIP Working Con-ference, Vienna, pages 197-220,1966.
[94]Bharath Sundararaman, Ugo Buy, and Ajay D. Kshemkalyani. Clock synchro-nization for wireless sensor networks:A survey. Ad Hoc Networks (Elsevier, 3:281-323,2005.
[95]Xinbci Tang and Jim Woodcock. Towards mobile processes in unifying theo-ries. In SEFM 2004:2nd International Conference on Software Engineering and Formal Methods, Beijing, China, September 26-30,2004, pages 44-53. IEEE Computer Society,2004.
[96]Xinbei Tang and Jim Woodcock. Travelling processes. In MPC 2004:7th International Conference on Mathematics of Program Construction, Stirling, Scotland, UK, July 12-14,2004, volume 3125 of Lecture Notes in Computer Science, pages 381-399. Springer-Verlag,2004.
[97]A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics,5:285-309,1955.
[98]Brett Warneke, Matt Last, Brian Liebowitz, and Kristofer S. J. Pister. Smart dust:Communicating with a cubic-millimeter computer. IEEE Computer, 34(1):44-51,2001.
[99]D. Watt. Programming Language Syntax and Semantics. Prentice Hall,1991.
[100]J. Woodcock and J. Davies. Using Z:Specification, Refinement, and Proof. Prcnticc-Hall,1996.
[101]Jim Woodcock and Ana Cavalcanti. The semantics of circus. In ZB 2002:2nd International Conference of B and Z Users, Grenoble, France, January 23-25, 2002, volume 2272 of Lecture Notes in Computer Science, pages 184-203. Springer,2002.
[102]Qiwen Xu, Willem P. de Rocvcr, and Jifeng He. The rely-guarantcc method for verifying shared variable concurrent programs. Formal Asp. Comput. 9(2):149-174,1997.
[103]Ming Zhou, Huabing Yang, Xingyuan Zhang, and Jinshuang Wang. The proof of aodv loop freedom. In WCSP 2009:International Conference on Wireless Communications Signal Processing, pages 1-5, Nov 2009.
[104]Huibiao Zhu, Jonathan P. Bowcn, and Jifcng He. Deriving operational seman-tics from denotational semantics for verilog. In APSEC 2001:8th Asia-Pacific Software Engineering Conference,4-7 December 2001, Macau, China, pages 177-184. IEEE Computer Society,2001.
[105]Huibiao Zhu, Jonathan P. Bowen, and Jifeng He. From operational semantics to denotational semantics for verilog. In CHARME 2001:11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Livingston, Scotland, UK, September 4-7,2001, volume 2144 of Lecture Notes in Computer Science, pages 449-466. Springer, 2001.
[106]Huibiao Zhu, Jonathan P. Bowen, and Jifeng He. Soundness, completeness and non-redundancy of operational semantics for verilog based on denota-tional semantics. In ICFEM 2002:4th International Conference on Formal Engineering Methods, Shanghai, China, October 21-25,2002, volume 2495 of Lecture Notes in Computer Science, pages 600-612. Springer,2002.
[107]Huibiao Zhu, Jifeng He, and Jonathan P. Bowen. From algebraic semantics to denotational semantics for verilog. In ICECCS 2006:11th International Conference on Engineering of Complex Computer Systems,15-17 August 2006, Stanford, California, USA, pages 139-151. IEEE Computer Society,2006.
[108]Huibiao Zhu, Jifeng He, and Jonathan P. Bowen. From algebraic semantics to denotational semantics for verilog. ISSE,4(4):341-360,2008.
[109]Huibiao Zhu, Jifeng He, and Jing Li. Unifying denotational semantics with operational semantics for web services. In ICDCIT 2007:4th International Conference on Distributed Computing and Internet Technology, Bangalore, India, December 17-20, volume 4882 of Lecture Notes in Computer Science, pages 225-239. Springer,2007.
[110]Huibiao Zhu, Jifcng He, Jing Li, and Jonathan P. Bowen. Algebraic approach to linking the semantics of web services. In SEFM 2007:5th IEEE Internation-al Conference on Software Engineering and Formal Methods,10-14 September 2007, London, England, UK, pages 315-328. IEEE Computer Society,2007.
[111]Huibiao Zhu, Jifeng He, Jing Li, and Jonathan P. Bowen. Algebraic approach to linking the semantics of web services. ISSE,7(3):209-224,2011.
[112]Huibiao Zhu, Jifcng He, Jing Li, Geguang Pu, and Jonathan P. Bowen. Linking denotational semantics with operational semantics for web services. ISSE, 6(4):283-298,2010.
[113]Huibiao Zhu, Gcguang Pu, and Jifeng He. A denotational approach to scope-based compensable flow language for web service. In ASIAN 2006:11th Asian Computing Science Conference, Tokyo, Japan, December 6-8,2006, volume 4435 of Lecture Notes in Computer Science, pages 28-36. Springer,2006.