{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T09:32:38Z","timestamp":1742635958804},"publisher-location":"Berlin, Heidelberg","reference-count":72,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540152040"},{"type":"electronic","value":"9783540393207"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15204-0_7","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:17:40Z","timestamp":1330193860000},"page":"101-121","source":"Crossref","is-referenced-by-count":5,"title":["Petri net based models for the specification and validation of protocols"],"prefix":"10.1007","author":[{"given":"Michel","family":"Diaz","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Azema","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"7_CR1","unstructured":"B. ALGAYRES, \"Sur la mod\u00e9lisation, la validation et l'impl\u00e9mentation d'un protocole de transport\", Th\u00e8se de Docteur-Ing\u00e9nieur, INSA, Toulouse, December 1982."},{"key":"7_CR2","unstructured":"J.P. ANSART et al, \"PDIL, un langage pour la description et l'impl\u00e9mentation de protocoles\", Journ\u00e9es ADI\/RHIN, Paris, 27\u201328 April 1983."},{"key":"7_CR3","unstructured":"J.M. AYACHE, P. AZEMA, M. DIAZ, \"Observer: a concept for on-line detection of control errors in concurrent systems\", IEEE Int. Symp. on Fault-Tolerant Computing, Madison, USA, June 1979."},{"key":"7_CR4","unstructured":"J.M. AYACHE, P. AZEMA, J.P. COURTIAT, M.DIAZ, G.JUANOLE \"On the applicability of Petri net based models in protocol design and verification\", Protocol Testing Workshop, NPL, Teddington, G.B., May 1981; Europ. Workshop on Application and Theory of Petri nets, Bad Honnef, RFA, Sept. 1981."},{"key":"7_CR5","unstructured":"J.M. AYACHE, J.P. COURTIAT, \"LC\/1, un langage pour la description, l'analyse et l'impl\u00e9mentation de protocoles\", Journ\u00e9es ADI\/RHIN, Paris, 27\u201328 April 1983."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"J.M. AYACHE, J.P. COURTIAT, M. DIAZ, \"REBUS: a fault-tolerant distributed system for industrial real time control\", IEEE T. on Computers Special Issue on Fault-Tolerant Computing, July 1982.","DOI":"10.1109\/TC.1982.1676061"},{"key":"7_CR7","unstructured":"J.M. AYACHE, J.P. COURTIAT, M. DIAZ, \"Self-checking software in distributed systems\", 3rd Conf. on Distributed Computing Systems, Miami, Nov. 1982."},{"key":"7_CR8","unstructured":"J.M. AYACHE, M. DIAZ, H. KONBER, \"Specification and verification of signalling protocols\", Int. Switching Symp., ISS 81, Montreal, Sept. 1981."},{"key":"7_CR9","unstructured":"P. AZEMA, B. BERTHOMIEU, P. DECITRE, \"The design and validation by Petri nets of a mechanism for the invocation of remote servers\", Proc. of IFIP Congress, Melbourne Oct. 1980."},{"key":"7_CR10","unstructured":"P. AZEMA, P. ROLIN, S. SEDILLOT, \"Virtual ring protection in distributed systems\", IEEE Int. Symp. on Fault-Tolerant Computing, Portland, Maine, USA, June 1981."},{"key":"7_CR11","unstructured":"B. BERTHOMIEU, M. MENASCHE, \"A state enumeration approach for analyzing time Petri nets\", 3rd Europ Workshop on Applications and Theory of Petri nets, Varenna, Italie, Sept. 1982."},{"key":"7_CR12","unstructured":"B. BERTHOMIEU, M. MENASCHE, \"An enumerative ap-proach for analyzing time Petri nets\", Proc. of the IFIP Congress, Paris, Sept. 1983."},{"key":"7_CR13","unstructured":"G. BERTHELOT, G. ROUCAIROL, R. VALK, \"Reduction of nets and parallel programs\", Net Theory and Applications, Lect. Notes in Computer Science, 45, Springer Verlag, 1977."},{"key":"7_CR14","unstructured":"G. BERTHELOT, R. TERRAT, \"Petri nets theory for the correctness of protocols\", 2nd Europ. Workshop on Appl. & Theory of Petri nets, Bad Honnef, RFA, Sept. 1981, pp. 31\u201358; also 2nd Int. Workshop on Protocol Specification Testing and Verification, Idyllwild Los Angeles, May 1982, North-Holland, 1982, C.Sunshine Ed."},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"B. BERTHOMIEU, \"Algebraic specification of communication protocols\", research Report ISI-RR-81-98, also Technical Report LAAS-CNRS, 81.T.26, Oct.1981.","DOI":"10.21236\/ADA111744"},{"key":"7_CR16","unstructured":"J. BILLINGTON, \"Specification of the transport service using numerical Petri nets\", 2nd Int. Worshop on Protocol Specification, testing and Verification, Idyllwild Los Angeles, May 1982, North-Holland, 1982, C. Sunshine Ed."},{"key":"7_CR17","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0376-5075(82)90098-8","volume":"6","author":"T. P. Blumer","year":"1982","unstructured":"T.P. BLUMER, R.L. TENNEY, \"A formal specification technique and implementation method for protocols\", Computer Networks 6, 1982, pp. 201\u2013217.","journal-title":"Computer Networks"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"G. BOCHMAN et al, \"Some experience with the use of formal specifications\", Proc. IFIP WG 6.1, 2nd Int. Workshop on Protocol Specification Testing and Verification, Idyllwild, May 1982.","DOI":"10.1016\/0376-5075(82)90113-1"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"G.V. BOCHMANN, \"Finite state description of communication protocols\", Conf. Computer Network Protocols, Li\u00e8ge 1978, also in Computer Networks 2, 1978, pp. 361\u2013372.","DOI":"10.1016\/0376-5075(78)90015-6"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"G.V. BOCHMANN, \"A general transition model for protocols and communication services\", IEEE Trans. on Communications, vol. COM-28, n\u00b04, April 1980, pp. 643\u2013650.","DOI":"10.1109\/TCOM.1980.1094696"},{"key":"7_CR21","unstructured":"G.V. BOCHMANN, J. GECSEI, \"A unified method for the specification and verification of protocols\", IFIP Proceedings, North-Holland, 1977."},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"G.V. BOCHMANN, C.A. SUNSHINE, \"Formal methods in communication protocol design\", IEEE Trans. on Com-munications, vol.COM-28, n\u00b04, April 1980, pp.624\u2013631.","DOI":"10.1109\/TCOM.1980.1094685"},{"key":"7_CR23","unstructured":"D. BRAND, P. ZAFIROPOULO, \"Synthesis of protocols for an unlimited number of processes\", Proc. of the Trends and Applications Symp., NBS, USA, May 1980."},{"key":"7_CR24","volume-title":"Un outil graphique interactif pour la validation des syst\u00e8mes \u00e0 \u00e9volution parall\u00e8le d\u00e9crits par r\u00e9seaux de Petri (OGIVE)","author":"B. Chezalviel-Pradin","year":"1979","unstructured":"B. CHEZALVIEL-PRADIN, \"Un outil graphique interactif pour la validation des syst\u00e8mes \u00e0 \u00e9volution parall\u00e8le d\u00e9crits par r\u00e9seaux de Petri (OGIVE)\", Th\u00e8se de Docteur-Ing\u00e9nieur, Universit\u00e9 Paul Sabatier, Toulouse, Dec. 1979."},{"key":"7_CR25","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1109\/TCOM.1980.1094686","volume":"COM-28","author":"A. Danthing","year":"1980","unstructured":"A. DANTHING, \"Protocol representation with finite-state models\", IEEE Trans. on Communications, vol.COM-28, n\u00b04 April 1980, pp.632\u2013643.","journal-title":"IEEE Trans. on Communications"},{"key":"7_CR26","unstructured":"A. DANTHINE, \"Petri nets for protocols modeling and verification\", IFIP-TC6, COMNET Symp., Budapest, Hong. Oct. 1977."},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"M. DEVY, M. DIAZ, \"Multilevel specification and validation of the control in communication systems\", 1st Int. Conf. on Distributed Computing Systems, Hunstville Alabama, Oct. 1\u20134, 1979.","DOI":"10.1016\/0306-4379(79)90011-5"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"M. DIAZ, \"Modeling and analysis of communication and cooperation protocols using Petri net based models\", Tutorial paper, Proc. of the IFIP WG 6.1 Second Int. Workshop on Protocol Specification, Testing and Verification, Idyllwid, CA, May 1982, C. Sunshine, Ed. North-Holland 1982; also Computer Networks, vol.6, n\u00b06, Dec. 1982.","DOI":"10.1016\/0376-5075(82)90112-X"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"M. DIAZ, J.P. COURTIAT, B. BERTHOMIEU, J.M. AYACHE, \"Status of Petri net based models for protocols\", IEEE Int. Conf. on Communications, ICC 83, Boston, June 1983.","DOI":"10.1145\/800056.802062"},{"key":"7_CR30","unstructured":"M. DIAZ, G. GUIDACCI DA SILVEIRA, \"On the specification and validation of protocols by temporal logic and nets\", Proceedings of the IFIP 83 Congress, Paris, Sept. 1983."},{"key":"7_CR31","unstructured":"B.L. DIVITO, \"Verification of communications protocols and abstract process models\", University of Texas at Austin, Technical Report 25, Aug. 1982."},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"P. ESTRAILLIER, C. GIRAULT, \"Petri nets specification of virtual ring protocols\", Proc. on the Applications and Theory of Petri nets, A. Pagnoni, G. Rozenberg Editors, IFB66, Springer Verlag, 1983, pp.74\u201385.","DOI":"10.1007\/978-3-642-69028-0_6"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"H.J. GENRICH, K. LAUTENBACH, \"The analysis of distributed systems by means of predicate\/transition nets\", Semantics of Concurrent Computation, Evian, 1979, G. Kahn ed., Lect. Notes in Computer Sciences vol.70, Springer Verlag 1979, pp.123\u2013146.","DOI":"10.1007\/BFb0022467"},{"key":"7_CR34","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-10001-6_22","volume":"84","author":"H. J. Genrich","year":"1980","unstructured":"H.J. GENRICH, K. LAUTENBACH, P.S. THIAGARAJAN, \"Elements of nets theory\", lect. Notes in Computer Science 84, 1980, pp.21\u2013163.","journal-title":"lect. Notes in Computer Science"},{"key":"7_CR35","unstructured":"S.L. GERHART et al, \"An overview of AFFIRM: a specification and verification system\", Proc. of the IFIP Congress, Oct. 1980, PP.343\u2013348."},{"key":"7_CR36","unstructured":"D.I. GOOD, R.M. COHEN, \"Verifiable communications processing in GYPSY\", Proc. of COMPCON 78, IEEE, Sept.78."},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"J. GUTTAG, \"Notes on type abstraction\", Proc. of the Conf. on Reliable Software, 1979, pp.170\u2013189.","DOI":"10.1007\/BFb0014684"},{"key":"7_CR38","unstructured":"G. GUIDACCI DA SILVEIRA, M. DIAZ, \"Une logique temporelle pour les syst\u00e8mes distribu\u00e9s\", Journ\u00e9es AFCET \"Protocoles et Syst\u00e8mes Distribu\u00e9s\", Paris, June 1981."},{"key":"7_CR39","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/TCOM.1983.1095720","volume":"COM-31","author":"B. T. Hailpern","year":"1983","unstructured":"B.T. HAILPERN, S.S. OWICKI, \"Modular verification of computer communication protocols\", IEEE T. on Communications, vol.COM-31, n\u00b01, January 1983, pp.56\u201368.","journal-title":"IEEE T. on Communications"},{"key":"7_CR40","unstructured":"ISO\/TC 97\/SC 16\/WG-FDT\/SG-C, \"ESTELLE Language for the specification of protocols\"."},{"key":"7_CR41","unstructured":"ISO\/TC 97\/SC 16\/WG-FDT\/SG-C, \"LOTOS Temporal ordering specification\"."},{"key":"7_CR42","unstructured":"G. JUANOLE, \"A data transfert protocol. Informal specification and modeling by Petri nets\", 2nd Europ. Workshop on the Theory and Applications of Petri nets, Bad Honnef, RFA, Sept. 1981, pp.347\u2013364."},{"key":"7_CR43","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"R. M. Keller","year":"1976","unstructured":"R.M. KELLER, \"Formal verification of parallel programs\" Com. ACM 19-7, vol.19, n\u00b07, July 1976, pp.371\u2013384.","journal-title":"Com. ACM 19-7"},{"key":"7_CR44","volume-title":"\"Sometimes is sometimes not never\", Proc. POPL, 1980","author":"L. Lamport","year":"1980","unstructured":"L. LAMPORT, \"Sometimes is sometimes not never\", Proc. POPL, 1980, ACM, Las Vegas, Jan. 1980."},{"key":"7_CR45","unstructured":"G. LE MOLI, \"A theory of colloquies\", Proc. of the 1st Europ. Workshop on Computer Network, Arles, April 1973."},{"key":"7_CR46","unstructured":"I. LOPEZ, \"The use of GALILEO to represent and analyse telecommunication protocols\", 2nd Eur. Workshop on the Theory and Application of Petri nets, Bad Honnef, FRG, September 1981, pp.397\u2013410."},{"key":"7_CR47","volume-title":"A study of the recoverability of computing systems","author":"P. M. Merlin","year":"1974","unstructured":"P.M. MERLIN, \"A study of the recoverability of computing systems\", Univ. of California, Irvine, 1974, Ph.D. Thesis."},{"key":"7_CR48","doi-asserted-by":"crossref","unstructured":"P.M. MERLIN, D.J. FARBER, \"Recoverability of communication protocols \u2014 implication of a theoritical study\", IEEE Trans.on Communications, Sept.1976, pp.1036\u20131043.","DOI":"10.1109\/TCOM.1976.1093424"},{"key":"7_CR49","unstructured":"OVIDE, Petri net validation tool, SYSECA, Jan. 1983."},{"key":"7_CR50","doi-asserted-by":"crossref","unstructured":"A. PNUELLI, \"The temporal logic of programs\", IEEE 18th Symp. on Foundations of Computer Science, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR51","unstructured":"J.B. POSTEL, \"A graph model analysis of computer communications protocols\", Ph.D. Thesis, Research Report UCLA, ENG\/7410, Jan. 1974."},{"key":"7_CR52","unstructured":"J.B. POSTEL, D. FARBER, \"Graph modeling of computer communications protocols\", Proc. 5th Texas Conf. on Computing Systems, Austin, 1976."},{"key":"7_CR53","unstructured":"J.P. QUEILLE, J. SIFAKIS, \"Specification and verification of concurrent systems in CESAR, an example\", 2nd Europ. Workshop on the Theory and Application of Petri nets, Bad Honnef, FRG, Sept. 1981, pp.483\u2013517."},{"key":"7_CR54","unstructured":"C. RAMCHANDANI, \"Analysis of asynchronous concurrent systems by timed Petri nets\", Research Report, Project MAC-TR 120, MIT, Feb. 1974."},{"key":"7_CR55","unstructured":"R. RAZOUK, \"Modelling X.25 using the graph model of behaviour\", 2nd Int.Workshop on Protocol Specification, Testing and Verification, Idyllwild Los Angeles, May 1982, North-Holland, 1982, C. Sunshine Ed."},{"key":"7_CR56","doi-asserted-by":"crossref","first-page":"1038","DOI":"10.1109\/TC.1980.1675509","volume":"C-29","author":"R. R. Razouk","year":"1980","unstructured":"R.R. RAZOUK, G. ESTRIN, \"Modelling and verification of communication protocols in SARA: the X.21 interface\", IEEE Trans. on Computers, vol.C-29, n\u00b012, Dec. 1980, pp.1038\u20131051.","journal-title":"IEEE Trans. on Computers"},{"key":"7_CR57","doi-asserted-by":"crossref","unstructured":"G. RICART, A.K. AGRAWALA, \"An optimal algorithm for mutual exclusion in computers networks\", Comm. of the ACM, 24, n\u00b01, Jan. 1981.","DOI":"10.1145\/358527.358537"},{"key":"7_CR58","doi-asserted-by":"crossref","unstructured":"D. SCHWABE, \"Formal specification and verification of a connection \u2014 establishment protocol\", Report ISI\/RR 81-91, USC\/ISI, April 1981.","DOI":"10.1145\/800081.802654"},{"key":"7_CR59","unstructured":"R.L. SCHWARTZ, P.M. MELLIAR-SMITH, \"Temporal logic specification of distributed systems\", 2nd Conf. Distributed Computing Systems, Paris, April 1981, pp.446\u2013454."},{"key":"7_CR60","doi-asserted-by":"crossref","unstructured":"R.L. SCHWARTZ, P.M. MELLIAR-SMITH, \"From state machine to temporal logic: specification methods for protocol standards\", Tutorial Paper, 2nd Workshop on Protocol Specification, Testing and Verification, Idyllwild Los Angeles, May 1982, North-Holland, 1982, C. Sunshine Ed., also IEEE Trans. on Communications, COM-30, n\u00b012, Dec. 1982, pp.2486\u20132496.","DOI":"10.1109\/TCOM.1982.1095451"},{"key":"7_CR61","first-page":"454","volume":"2","author":"C. A. Sunshine","year":"1978","unstructured":"C.A. SUNSHINE, Y.K. DALAL, \"Connection management in transport protocols\", Computer Networks 2, Dec. 1978, pp.454\u2013473.","journal-title":"Computer Networks"},{"key":"7_CR62","first-page":"346","volume":"2","author":"C. A. Sunshine","year":"1978","unstructured":"C.A. SUNSHINE, \"Survey of protocol definition and verification techniques\", Computer Networks, 2, 1978, pp.346\u2013350.","journal-title":"Computer Networks"},{"key":"7_CR63","unstructured":"C.A. SUNSHINE, \"Formal modelling of communication protocols\", ISI-USC report RR-81-89, March 1981; 1st Workshop on Protocol Testing, NPL, Teddington, GB, May 1981."},{"key":"7_CR64","unstructured":"F.J.W. SYMONS, \"Modelling and analysis of communication protocols using numerical Petri nets\", Ph.D. Thesis, University of Essex, Being Dept. of Elect. Eng. Sc. Telecomm. Syst. Group Report n\u00b0152, May 1978."},{"key":"7_CR65","unstructured":"F.J.W. SYMONS, \"Representation, analysis and verification of communication protocols\", Research Report 7380, Telecom., Australia, 1980."},{"key":"7_CR66","unstructured":"D.T. THOMPSON, C.A. SUNSHINE, R.W. ERICKSON, S.L. GERHART, D. SCHWABE, \"Specification and verification of communication protocols in AFFIRM using state transition models\", Research Report ISI-RR-81-88, USC, Inf. Sc. Institute, March 1981."},{"key":"7_CR67","unstructured":"F. VIDONDO, \"GALILEO, experiences in the design of a Petri net based language for real-time systems\", 2nd Eur. Workshop on the Theory and Application of Petri nets, Bad Honnef, FRG, Sept. 1981, pp.541\u2013550."},{"key":"7_CR68","doi-asserted-by":"crossref","first-page":"539","DOI":"10.1109\/TSE.1980.234502","volume":"6","author":"K. Voss","year":"1980","unstructured":"K. VOSS, \"Using predicate\/transition-nets to model and analyze distributed database systems\", IEEE Trans. on Software Eng., vol.6, n\u00b06, Nov.1980, pp.539\u2013544.","journal-title":"IEEE Trans. on Software Eng."},{"key":"7_CR69","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1147\/rd.224.0393","volume":"22","author":"C. H. West","year":"1978","unstructured":"C.H. WEST, \"General technique for communications protocols validation\", IBM J. Research Develop., vol.22, July 1978, pp.393\u2013404.","journal-title":"IBM J. Research Develop."},{"key":"7_CR70","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1147\/rd.221.0060","volume":"22","author":"C. West","year":"1978","unstructured":"C. WEST, P. ZAFIROPOULO, \"Automated validation of a communication protocol: the CCITT X.21 recommendation\", IBM J.R. and Develop., vol.22, Jan.1978, pp.60\u201371","journal-title":"IBM J.R. and Develop."},{"key":"7_CR71","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1109\/TCOM.1980.1094687","volume":"COM-28","author":"P. Zafiropoulo","year":"1980","unstructured":"P. ZAFIROPOULO et al, \"Towards analyzing and synthesizing protocols\", IEEE Trans. on Communications, COM-28, April 1980, pp.651\u2013661.","journal-title":"IEEE Trans. on Communications"},{"key":"7_CR72","doi-asserted-by":"crossref","unstructured":"H. ZIMMERMAN, \"OSI reference model. The ISO model of architecture for open systems interconnection\", IEEE Trans. on Communications, vol.COM-28, April 1980.","DOI":"10.1109\/TCOM.1980.1094702"}],"container-title":["Lecture Notes in Computer Science","Advances in Petri Nets 1984"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15204-0_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:08:18Z","timestamp":1605643698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15204-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540152040","9783540393207"],"references-count":72,"URL":"https:\/\/doi.org\/10.1007\/3-540-15204-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1985]]}}}