摘要
随着计算机网络、通信网络以及分布式系统的不断发展，通信协议有日渐复杂
化的趋势，形式描述技术在网络协议设计中占有举足轻重的作用，作为国际化标准
之一的LOTOS技术是专为分布式系统设计的形式描述技术，特别是通信服务和协议。
本文对LOTOS技术在网络通信协议设计中的应用方法进行了研究。归纳总结了
基于LOTOS的形式化描述方法、形式化的转换、验证和实现等方法理论，以及通信
服务和协议的构造方法及服务规范到协议规范的等效性转换方法，重点研究了规范
风格和结构概念在服务和协议设计中的应用。
文章主要由四部分构成：
第一部分：简要介绍了形式描述技术在协议工程中的应用范围，LOTOS技术的
背景和发展状况(第一章)；然后介绍了LOTOS的语言基础(第二章)。
第二部分：详细描述了在网络协议设计中基于LOTOS相关技术的应用领域及在
这些领域中的应用方法，包括：LOTOS规范风格、LOTOS转换、LOTOS验证、LOTOS
实现、ELOTOS以及LOTOS工具集等(第三章)。
第三部分：详细论述了通信模型的构造方法，服务规范和协议规范的构造方法，
及将服务规范转变为协议规范的方法(第四章)。
第四部分：提出了LOTOS规范风格在网络服务和协议设计中的应用方法、形式
结构模型的概念及实现方法、面向宏的概念及实现方法、LOTOS规范的C、C++实现
方法(第五章)；并举一案例说明基于LOTOS技术的协议设计方法(第六章)。
With the further development of computer network, communication network and the distributed system, communication protocols are more and more complicated, formal description technology plays the indispensable role in the network protocol design. LOTOS - as one of the ISO standards of FDT, is designed for distributed systems, especially for communication service and communication protocol.
In this paper, the application of LOTOS technology in network communication protocol design is studied. The formal description technology based on LOTOS, the formal transformation, the formal validation and implemenation are generalized. Constructions of communication service and communication protocol, transformation from service specification into protocol specification based on bisimulation equivalence are also stated in detail. Application of LOTOS specification styles and architecture concept in service and protocol design is studied as an emphasis.
This paper mainly including four parts:
The first one: Briefly introduced the application field of ADT in protocol project, the background and the development of LOTOS technology; then described the foundation of LOTOS language.
The second one: Discussed the application spectrum of technology based on LOTOS in network protocol design in detail, which including LOTOS specification styles, LOTOS transformation, LOTOS validation, LOTOS implementation, ELOTOS and LOTOS toolkit, etc.
The third one: Described the composition of communication model, construction of service specification and protocol specification, and the approach of transform service specification into protocol specification.
The last one: Produced the application method of LOTOS specification styles in network service and protocol design, the concept of formal structural model and its design approach, Macro-oriented specification style and its implementation, the transformation of LOTOS specification to C or C++. Then an example is taken to illustrate how to use the ADT to describle a protocol.
引文
[1] 龚正虎．计算机网络协议工程[M]．长沙：国防科技大学出版社，1993，12．
[2] 古天龙，蔡国庆．网络协议的形式化分析与设计[M]．北京：电子工业出版 社，2003，6．
[3] 卢锡城，龚正虎等．先进计算机网络技术．北京：国防工业出版社， 2002，10．
[4] 李腊元．通信协议形式化模型的研究[J]．计算机学报，1998，21(5) ： 419-427．
[5] 李腊元，计算机网络协议的形式描述风格[J]，计算机工程与设计 (1994：3) ：9-18．
[6] http://www. cims. edu. cn/MonographicTech/support/Intranet/confer.ht m
[7] http://www. run. montefiore. ulg. ac. be/Research/Topics/index. php?top ic=Lotos
[8] http://www. cs. stir. ac. uk/~kjt/research/well/well. html
[9] ISO/IEC 8807, Information Processing Systems, Open Systems Interconnection, LOTOS-A Formai Description Technique Based on the Temporai Ordering of Observational Behaviour [S], 1989．
[10] http://www. dit. upm. es/~lotos/elotos. html
[11] Milner, R. A Calculus of Communicating Systems. Lecture Notes in Computer Science[C], Vol. 92, Springer-Verlag, 1980．
[12] Hoare, C. A. R. Communicating Sequential Processes [M]. Prentice-Hall, 1985．
[13] Bolognesi, B., and Brinksma, E. Introduction to the ISO Specification Language LOTOS [J]. Computer Networks and ISDN Systems, 1987(14) : 25-59．
[14] http://www. inrialpes. fr/vasy/eucalyptus. html
[15] http://www-run. montefiore. ulg. ac. be/projects/EUCALYPTUS. html
[16] C. A. Vissers, G. Scollo, M. van Sinderen, E. Brinksma. Specification Styles in Distributed Systems Design and Verification [C]. Theoretical Computer Science, North-Holland, 1991: 179-206．
[17] Lotosphere Project ESPRIT 2304． Lo/WP1/T1． 1/N0045/V04-The Lotosphere Design Methodology: Basic Concepts [R]. march 1992．
[18] Neil Hart. Protocol Validation and Implementation: A Design Methodology Using LOTOS and ROOM [D]. Ottawa, University of Ottawa, 1998．
[19] Lotosphere Project ESPRIT 2304． Lo/WP1/T1． 1/N0044/V04-The Lotosphere Design Methodology: Guidelines [R]. march 1992．
[20] P.H.van Eijk, H. Kremer, and M. van Sinderen. On the use of Specification styles for automated protocol implementation from LOTOS
to C [J]. In Tenth International IFIP WG 6． l Symposium on Protocol Specification, Testing and Verification. North Holland, 1990．
[21] C. A. Vissers, G. Scollo, and M. van Sinderen. Architecture and specification style in formai descriptions of distributed systems [C]. In S. Aggarwal and K. Sabnani, editors, Protocol Specification, Testing, and Verification, Ⅷ, pages 189-204． North-Holland, 1998．
[22] J.-P. Courtiat. The Lotosphere design methodology:Illustrations [R]. ESPRIT 2304 Lotosphere project, February 1992．
[23] T. Bolognesi. Lo/WP1/Tl. 2/N0033/V02-correctness preserving transformation-taskl. 2 second deliverable [R]. Lotosphere Project, april 1990．
[24] T. Bolognesi. Catalogue of LOTOS transformation [R]. ESPRIT 2304 Lotosphere project, February 1992．
[25] A. Fernandez, J. Quemada, L. Vidaller, and C. Miguel. PRODAT-The Derivation of an Implementation from its LOTOS Formai Description [R]. In Protocol Specification, Testing and Verification Ⅷ, Atlantic City, June 1988．
[26] ESA. Software engineering standards [R]. BSSCESA.1987．
[27] IEEE. IEEE Software Engineering Standards [S]. IEEE-John Wiley, 1987． ISBN 471-63457-3．
[28] R. De Nicola and M. C. B. Hennessy. Testing equivalentces for processes [J]. Theory of Computer Science, pages 83-133, 1984．
[29] S. Abramsky. Observational equivalentce as a testing equivalentce [J]. Theoretical Computer Science, pages 225-241, 1987．
[30] E. Brinksma and G. Scollo. Formai notions of implementation and conformance in LOTOS-Memorandum INF-86-13[R]. Twente University of Technology, December 1986．
[31] S. Colwill. Lo/WP3/T3． 3/BT/N0018/V01-towards machine-assisted formai validation of LOTOS specifications[R]. BT, December 1990．
[32] G. Burtwistle and P. Subrahmanyam, editors. VLSI Specification, Verification and Synthesis, chapter A Proof Generating System for Higher-Order Logic (by M. Gordon)[J], pages 73-128． Kluwer Academic Publishers, Boston, 1988．
[33] A. Wikstrom. Functional Programming Using Standard ML [M]. Prentice Hall.
[34] ISO/IEC. Information Technology-E-LOTOS [S]. 2001．
[35] M. Nakamura, Y. Kakuda, and T.Kikuno. On constructing comm. unication protocols from component-based service specifications [J]. Computer Communications, (19) : 1200-1215, 1996．
[36] E. Brinksma, R. Langerak, and P. Broekroelofs. Functionality decomposition by compositional correctnesss preserving transformation [J]. In Computer Aided Verification (CAV), pages 371-384, 1993．
[37] B. B. Bista, K.Takahashi, and N. Shiratori. Composition of protocol functions. IEICE Trans. On Fundamentals of Electronics [J], Communications and Computer Sciences, E81-A(4) :586-595, April 1998．
[38] H.-A. Lin. Constructing protocols with alternative functions [J]. IEEE Transactions on Computers, 40(4) :376-386,April 1991．
[39] H.-A. Lin and C.-L Tarng. An improved method for constructing multiphase Communications protocols [J]. IEEE Transactions on Computers, 42(1) :15-26, January 1993．
[40] G. Singh. A compositional approach for designing protocols [J]. In Proceedings of the International Conference on Network Proceedings, pages 98-105, San Francisco, California, 19-22 October 1993． IEEE Computer Society.
[41] B. B. Bista, K. Takahashi, and N. Shiratori. Composition of service and protocol specifications [J]. In Proceedings of the 15th International Conference on Information Networking, pages 171-178, Beppu City, Oita, Japan, 31 Jan-2 Feb 2001． IEEE Computer Society Press.
[42] G. Singh, I. Buricea, and Z. Mao. Composition of service specifications [J]. In Proceedings of the International Conference on Network Protocols (ICNP98) , pages 210-218． IEEE Computer Society. 1998．
[43] R. Langerak. Decomposition of functionality: a correctnesss preserving LOTOS transformation [C]. In L. Logrippo, R. L. Probert, and H. Ural, editors, Protocol Specification, Testing and Verification, X, pages 203-218． North-holland, June 1990．
[44] L. Bellissard, N. De Palma, A. Freyssinet, M. Herrmann, and S. Lacourte. An Agent Platform for Reliable Asynchronous Distributed Programming [C]. In Proceedings of the Symposium on Reliable Distributed Systems SRDS'99 (Lausanne, Suisse), October 1999．
[45] N. De Palma, L. Bellissard, D. F_eliot, A. Freyssinet, M. Herrmann, and S. Lacourte. The AAA Agent-based Message Oriented Middleware [R]. C3DS Public Technical Report Series 30, ESPRIT Long Terra Research Project no. 24962, 2000．
[46] N. De Palma, L. Bellissard, and M. Riveill. Dynamic Recon_guration of Agent-Based Applications [C]. In Proceedings of the 3rd European Research Seminar on Advances in Distributed Systems ERSADS'99 (Madeira Island, Portugal), April 1999．
[47] M. Raynal, A. Schiper, and S. Toueg. The Causai Ordering Abstraction and a Simple Way to Implement It [J]. Information Processing Letters, 39(6) :343-350, 1991．
[48] P. Laumay, E. Bruneton, L. Bellissard, and S. Krakowiak. Preserving Causality in a Scalable Message-Oriented Middleware [R]. C3DS 3rd Year Report Deliverable, ESPRIT Long Term Research Project no. 24962, 2001．