This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Protocol Modeling and Verification Approach Based on a Specification Language and Petri Nets
May 1990 (vol. 16 no. 5)
pp. 523-536

An approach for automated modeling and verification of communication protocols is presented. A language that specifies the input/output behavior of protocol entities is introduced as the starting point of the approach, and verification of the linguistic specifications is discussed. Rules for conversion of the specifications into a Petri net model (based on a timed Petri net) are presented and illustrated by examples. This leads to a second level of verification on the net model. The approach is illustrated by its application to a part of the LAPD protocol.

[1] IEEE Trans. Software Eng. (Special Issue on Tools for Computer Communication Systems), vol. 14, no. 3, Mar. 1988.
[2] T. Murata, "Modeling and analysis of concurrent systems," inHandbook of Software Engineering, C. R. Vick and C. V. Ramamoorthy, Eds. New York: Van Nostrand Reinhold, 1984, ch. 3, pp. 39-63.
[3] J. L. Peterson,Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.
[4] J. Billington, "Protocol engineering and nets," inProc. Eighth European Workshop Application and Theory of Petri Nets, June 1987, pp. 137-156.
[5] G. R. Wheeler, M. C. Wilbur-Ham, J. Billington, and J. A. Gilmour, "Protocol analysis using Numerical Petri Nets,"Advances in Petri Nets 1985, (Lecture Notes in Computer Science, vol. 222). Berlin: Springer-Verlag, 1986, pp. 435-452.
[6] P. M. Merlin, "A methodology for the design and implementation of communication protocols,"IEEE Trans. Commun., vol. COM-24, no. 6, pp. 614-621, June 1976.
[7] R. R. Razouk and C. V. Phelps, "Performance analysis using timed Petri nets," inProtocol Specification, Testing, and Verification, IV, Y. Yemini, R. Strom, and S. Yemini, Eds. New York: Elsevier, 1985, pp. 561-576.
[8] C. V. Ramamoorthy, S. T. Dong, and Y. Usuda, "An implementation of an automated protocol synthesizer (APS) and its application to the X.21 protocol,"IEEE Trans. Software Eng., vol. SE-11, no. 9, pp. 886-908, Sept. 1985.
[9] P. M. Merlin and G. V. Bochman, "On the construction of communication protocols," inProc. 5th Int. Conf. Computer Communication, 1980.
[10] S. M. Shatz and D. Xie, "Petri net modeling and analysis of the LAPD protocol standard: Methods and results," inProc. 11th Int. Computer Software and Applications Conf., Oct. 1987, pp. 694-699.
[11] I. Lopez and M. C. Pelaez, "Experiences in the use of GALILEO to design telecommunication systems," inProc. Eighth European Workshop Application and Theory of Petri Nets, June 1987, pp. 175- 196.
[12] G. V. Bochmann and C. A. Sunshine, "Formal methods in communication protocol design,"IEEE Trans. Commun., vol. COM-28, no. 4, pp. 624-631, Apr. 1980.
[13] E. Brinksma, "A tutorial on LOTOS," inProc. 5th IFIP Symp. Protocol Spec. Test. Verif., June 1985.
[14] R. J. Linn, "The features and facilities of Estelle: A formal description technique based upon an extended finite state machine model," inProtocol, Specification, Testing, and Verification V, M. Diaz, Ed. Amsterdam, The Netherlands: North-Holland, 1986, pp. 271-296.
[15] D. P. Anderson, "Automated protocol implementation with RTAG,"IEEE Trans. Software Eng., vol. 14, no. 3, pp. 291-300, Mar. 1988.
[16] CCITT, "Data communication networks: Open systems interconnection (OSI), system description techniques,"Red Book, Recommendations X.200-X.250, 1984.
[17] S. Aggarwal, D. Barbara, and K. Meth, "A software environment for the specification and analysis of problems of coordination and concurrency,"IEEE Trans. Software Eng., vol. 14, no. 3, pp. 280-290, Mar. 1988.
[18] H. Ichikawa, M. Itoh, and J. Kato, "Communication software management with verification and transformation of protocol-oriented specifications," inProc. IEEE Globecom '87, Nov. 1987, pp. 651- 655.
[19] CCITT, "Specification of signaling system no. 7,"Red Book, Recommendations Q.701-Q.714, 1984.
[20] Y. Wakahara and K. Kakuda, "Verification of requirements specifications for telecommunications software by the investigation of specifications execution sequences," inProc. IEEE Globecom '87, Nov. 1987, pp. 661-666.
[21] K. Rea and R. de B. Johnston, "Automated analysis of discrete communication behavior,"IEEE Trans. Software Eng., vol. SE-13, no. 10, pp. 1115-1126, Oct. 1987.
[22] E. T. Morgan and R. R. Razouk, "Interactive state-space analysis of concurrent systems,"IEEE Trans. Software Eng., vol. SE-13, pp. 1080-1091, Oct. 1987.
[23] E. T. Morgan and R. R. Razouk, "Computer-aided analysis of concurrent systems," inProtocol Specification, Testing, and Verification, V. M. Diax, Ed. New York: North Holland, 1986, pp. 49-58.
[24] M. Hack, "Analysis of production schemata by Petri nets," M.S. thesis, Dep. Elec. Eng., Massachusetts Inst. Technol., Cambridge, 1972.
[25] Digital Multiplexed Interface, AT amp;T, Tech. Specification, Issue 3.1, 1986.

Index Terms:
conversion rules; specification language; Petri nets; automated modeling; verification; communication protocols; input/output behavior; linguistic specifications; timed Petri net; LAPD protocol; Petri nets; program verification; protocols; specification languages.
Citation:
T. Suzuki, S.M. Shatz, T. Murata, "A Protocol Modeling and Verification Approach Based on a Specification Language and Petri Nets," IEEE Transactions on Software Engineering, vol. 16, no. 5, pp. 523-536, May 1990, doi:10.1109/32.52775
Usage of this product signifies your acceptance of the Terms of Use.