
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
I. Suzuki, "Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets," IEEE Transactions on Software Engineering, vol. 16, no. 11, pp. 12731281, November, 1990.  
BibTex  x  
@article{ 10.1109/32.60315, author = {I. Suzuki}, title = {Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets}, journal ={IEEE Transactions on Software Engineering}, volume = {16}, number = {11}, issn = {00985589}, year = {1990}, pages = {12731281}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.60315}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets IS  11 SN  00985589 SP1273 EP1281 EPD  12731281 A1  I. Suzuki, PY  1990 KW  formal analysis; formal verification; alternating bit protocol; temporal Petri nets; firings; transitions; formulas; temporal operators; formal specification; omega regular expressions; Buchiautomata; automata theory; formal specification; Petri nets; program verification; programming theory VL  16 JA  IEEE Transactions on Software Engineering ER   
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 Buchiautomata.
[1] B. Alpern and F. B. Schneider, "Verifying temporal properties without temporal logic,"ACM Trans. Program. Lang. Syst., vol. 11, no. 1, pp. 147167, Jan. 1989.
[2] K. A. Bartlett, R. A. Scantlebury, and P.T. Wilkinson, "A note on reliable fullduplex transmission over halfduplex link,"Commun. ACM, vol. 12, no. 5, May 1969.
[3] J. R. Büchi, "On a decision method in restricted secondorder 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. 117141, 1974.
[5] H. J. Genrich and K. Lautenbach, "System modelling with highlevel Petri nets,"Theoretical Comput. Sci., vol. 13, pp. 109136, 1981.
[6] B. Hailpern and S. Owicki, "Modular verification of computer communication protocols,"IEEE Trans. Comm., vol. COM31, Jan. 1983.
[7] S. C. Kleene, "Representation of events in nerve nets and finite automata," inAutomata Studies. Princeton, NJ: Princeton University Press, 1956, pp. 341.
[8] L. Lamport, "Specifying Concurrent ProgramModules,"ACM Trans. Programming Languages and Systems, Vol. 5, No. 2, Apr. 1983, pp. 190222.
[9] L. H. Landweber, "Decision problems forωautomata,"Math. Syst. Theory, vol. 3, no. 4, pp. 376384, 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. 823826.
[11] W. C. Lynch, "Reliable fullduplex file transmission over halfduplex telephone lines,"Commun. ACM, vol. 11, no. 6, pp. 407 410, June 1968.
[12] Z. Manna,Mathematical Theory of Computation. New York: McGrawHill, 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. 93122, May 1984.
[14] R. McNaughton, "Testing and generating infinite sequences by a finite automaton,"Inform. Contr., vol. 9, pp. 521530, 1966.
[15] P. Merlin and D.J. Faber, "Recoverability of communication protocols,"IEEE Trans. Commun, vol. COM24, 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. 541580, Apr. 1989.
[18] M. Nivat, "Behavior of processes and synchronized systems of processes, " inTheoreticalFoundations of Programming Methodology, M. Broy and G. Schmidt, Eds. Dordrecht, The Netherlands: Reidel, 1982, pp. 473551.
[19] D. Park, "Concurrency and automata on infinite sequences," inProc. 5th GIConf. Theoretical Comput. Sci., Lecture Notes in Computer Science 104. New York: SpringerVerlag, 1981, pp. 167183.
[20] J. L. Peterson, "Petri nets,"ACM Comput. Surveys, vol. 9, no. 3, pp. 223252, Sept. 1977.
[21] C. V. Ramamoorthy and G. S. Ho, "Performance evaluation of asynchronous concurrent systems using Petri nets,"IEEE Trans. Software Eng., vol. SE6, no. 5, pp. 440449, 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. MelliarSmith, "Temporal logic specification of distributed systems," inProc. 2nd Int. Conf. Distributed Computing Systems. Washington, DC: IEEE Computer Society Press, 1981, pp. 446454.
[24] R. L. Schwartz and P. M. MelliarSmith, "From state machines to temporal logic: specification methods for protocol standards,"IEEE Trans. Commun., vol. COM30, pp. 24862496, 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. 641646.
[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. C38, no. 5, pp. 696704, 1989.
[27] M. Takahashi and H. Yamasaki, "A note onωregular languages,"Theoretical Comput. Sci., vol. 23, pp. 217225, 1983.
[28] A. Tarski, "A latticetheoretical fixpoint theorem and its applications,"Pacific J. Math., vol. 5, pp. 285309, 1955.
[29] R. Valk, "Infinite behavior of Petri nets,"Theoretical Comput. Sci., vol. 25, pp. 311341, 1983.
[30] M. Y. Vardi and P. Wolper, "An automatatheoretic approach to automatic program verification," inProc. IEEE Symp. Logic in Computer Science, Boston, MA, 1986, pp. 332344.