This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets
November 1990 (vol. 16 no. 11)
pp. 1273-1281

Temporal Petri nets are Petri nets in which certain restrictions on the firings of transitions are represented by formulas containing temporal operators. The use of temporal Petri nets for formal specification and verification of the alternating bit protocol is discussed. The temporal Petri net which models the protocol is analyzed formally using the existing theory of omega -regular expressions and Buchi-automata.

[1] B. Alpern and F. B. Schneider, "Verifying temporal properties without temporal logic,"ACM Trans. Program. Lang. Syst., vol. 11, no. 1, pp. 147-167, Jan. 1989.
[2] K. A. Bartlett, R. A. Scantlebury, and P.T. Wilkinson, "A note on reliable full-duplex transmission over half-duplex link,"Commun. ACM, vol. 12, no. 5, May 1969.
[3] J. R. Büchi, "On a decision method in restricted second-order arithmetic," inProc. Int. Congr. Logic Methodology and Philosophy of Sciences 1960. Stanford CA: Stanford University Press, 1962.
[4] Y. Choueka, "Theories of automata onω-tapes: A simplified approach,"J. Comput. Syst. Sci., vol. 8, pp. 117-141, 1974.
[5] H. J. Genrich and K. Lautenbach, "System modelling with high-level Petri nets,"Theoretical Comput. Sci., vol. 13, pp. 109-136, 1981.
[6] B. Hailpern and S. Owicki, "Modular verification of computer communication protocols,"IEEE Trans. Comm., vol. COM-31, Jan. 1983.
[7] S. C. Kleene, "Representation of events in nerve nets and finite automata," inAutomata Studies. Princeton, NJ: Princeton University Press, 1956, pp. 3-41.
[8] L. Lamport, "Specifying Concurrent ProgramModules,"ACM Trans. Programming Languages and Systems, Vol. 5, No. 2, Apr. 1983, pp. 190-222.
[9] L. H. Landweber, "Decision problems forω-automata,"Math. Syst. Theory, vol. 3, no. 4, pp. 376-384, 1969.
[10] H. Lu and I. Suzuki, "Application of temporal Petri nets to verification of handshake daisy chain arbiters," inProc. 29th Midwest Symp. Circuits and Systems, Lincoln, NE, 1987, pp. 823-826.
[11] W. C. Lynch, "Reliable full-duplex file transmission over half-duplex telephone lines,"Commun. ACM, vol. 11, no. 6, pp. 407- 410, June 1968.
[12] Z. Manna,Mathematical Theory of Computation. New York: McGraw-Hill, 1974.
[13] M. Ajmone Marsan, G. Balbo, and G. Conte, "A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems,"ACM Trans. Comput. Syst., vol. 2, pp. 93-122, May 1984.
[14] R. McNaughton, "Testing and generating infinite sequences by a finite automaton,"Inform. Contr., vol. 9, pp. 521-530, 1966.
[15] P. Merlin and D.J. Faber, "Recoverability of communication protocols,"IEEE Trans. Commun, vol. COM-24, no. 9, Sept. 1976.
[16] M. K. Molloy, "On the integration of delay and throughput measures in distributed processing models," Ph.D. dissertation, Dep. Comput. Sci., Univ. of California, Los Angles, 1981.
[17] T. Murata, "Petri nets: Properties, analysis, and applications,"Proc. IEEE, vol. 77, no. 4, pp. 541-580, Apr. 1989.
[18] M. Nivat, "Behavior of processes and synchronized systems of processes, " inTheoretical-Foundations of Programming Methodology, M. Broy and G. Schmidt, Eds. Dordrecht, The Netherlands: Reidel, 1982, pp. 473-551.
[19] D. Park, "Concurrency and automata on infinite sequences," inProc. 5th GI-Conf. Theoretical Comput. Sci., Lecture Notes in Computer Science 104. New York: Springer-Verlag, 1981, pp. 167-183.
[20] J. L. Peterson, "Petri nets,"ACM Comput. Surveys, vol. 9, no. 3, pp. 223-252, Sept. 1977.
[21] C. V. Ramamoorthy and G. S. Ho, "Performance evaluation of asynchronous concurrent systems using Petri nets,"IEEE Trans. Software Eng., vol. SE-6, no. 5, pp. 440-449, Sept. 1980.
[22] C. Ramchandani, "Analysis of asynchronous concurrent systems by timed Petri nets," Massachusetts Inst. Technol., Project MAC, Tech. Rep. 120, Feb. 1974.
[23] R. L. Schwartz and P. M. Melliar-Smith, "Temporal logic specification of distributed systems," inProc. 2nd Int. Conf. Distributed Computing Systems. Washington, DC: IEEE Computer Society Press, 1981, pp. 446-454.
[24] R. L. Schwartz and P. M. Melliar-Smith, "From state machines to temporal logic: specification methods for protocol standards,"IEEE Trans. Commun., vol. COM-30, pp. 2486-2496, Dec. 1982.
[25] I. Suzuki, "Fundamental properties and applications of temporal Petri nets," inProc. 9th Annu. Conf. Information Sciences and Systems, Johns Hopkins Univ., Baltimore, MD, 1985, pp. 641-646.
[26] I. Suzuki and H. Lu, "Temporal Petri nets and their application to modeling and analysis of a handshake daisy chain arbiter,"IEEE Trans. Comput., vol. C-38, no. 5, pp. 696-704, 1989.
[27] M. Takahashi and H. Yamasaki, "A note onω-regular languages,"Theoretical Comput. Sci., vol. 23, pp. 217-225, 1983.
[28] A. Tarski, "A lattice-theoretical fixpoint theorem and its applications,"Pacific J. Math., vol. 5, pp. 285-309, 1955.
[29] R. Valk, "Infinite behavior of Petri nets,"Theoretical Comput. Sci., vol. 25, pp. 311-341, 1983.
[30] M. Y. Vardi and P. Wolper, "An automata-theoretic approach to automatic program verification," inProc. IEEE Symp. Logic in Computer Science, Boston, MA, 1986, pp. 332-344.

Index Terms:
formal analysis; formal verification; alternating bit protocol; temporal Petri nets; firings; transitions; formulas; temporal operators; formal specification; omega -regular expressions; Buchi-automata; automata theory; formal specification; Petri nets; program verification; programming theory
Citation:
I. Suzuki, "Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets," IEEE Transactions on Software Engineering, vol. 16, no. 11, pp. 1273-1281, Nov. 1990, doi:10.1109/32.60315
Usage of this product signifies your acceptance of the Terms of Use.