{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T08:27:41Z","timestamp":1742632061908},"reference-count":84,"publisher":"Elsevier BV","issue":"14","license":[{"start":{"date-parts":[[1996,12,1]],"date-time":"1996-12-01T00:00:00Z","timestamp":849398400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer Communications"],"published-print":{"date-parts":[[1996,12]]},"DOI":"10.1016\/s0140-3664(96)01158-9","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T11:13:42Z","timestamp":1027595622000},"page":"1250-1257","source":"Crossref","is-referenced-by-count":8,"title":["Petri nets for protocol engineering"],"prefix":"10.1016","volume":"19","author":[{"given":"To-yat","family":"Cheung","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0140-3664(96)01158-9_BIB1","series-title":"Xth Int. Conf. Applic. & Theory of Petri nets","first-page":"67","article-title":"Modeling and simulation of a communication protocol by SWN, Tutorial","author":"Chiola","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB2","series-title":"High-Level Petri nets","first-page":"691","article-title":"Computer tools for high-level Petri nets","author":"Feldbrugge","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB3","first-page":"2","article-title":"Petri net tool overview","volume":"41","author":"Feldbrugge","year":"1992","journal-title":"Petri net Newsletter"},{"issue":"4\/5","key":"10.1016\/S0140-3664(96)01158-9_BIB4","first-page":"381","article-title":"Modelling and verification of end-to-end transport protocols","volume":"2","author":"Danthine","year":"1978","journal-title":"Computer Networks"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB5","first-page":"419","article-title":"Modeling and analysis of communication and cooperation protocols using Petri net based models","volume":"6","author":"Diaz","year":"1982","journal-title":"Computer Networks"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB6","series-title":"Petri nets: Central Model and their Properties","article-title":"Petri net based models in the specification and verification of protocol","author":"Diaz","year":"1987"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB7","first-page":"165","article-title":"Modelling of OSI-communication services and protocols using predicate\/transition nets, Protocol Specification, Testing and Verification-FV","author":"Burkhardt","year":"1984"},{"issue":"3","key":"10.1016\/S0140-3664(96)01158-9_BIB8","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1109\/32.4651","article-title":"PROTEAN: a high-level Petri net tool for the specification and verification of communication protocols","volume":"SE-14","author":"Billington","year":"1988","journal-title":"IEEE Trans. Soft. Eng."},{"key":"10.1016\/S0140-3664(96)01158-9_BIB9","series-title":"Proc. COMNET'85","first-page":"6.103","article-title":"PNPUO \u2014 A Petri net based software package for protocol validation","author":"Cheung","year":"1985"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB10","first-page":"219","article-title":"Time streams Petri nets: a model for timed multimedia information","volume":"815","author":"Diaz","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB11","first-page":"62","article-title":"Timed Petri net schedules","volume":"340","author":"Carlier","year":"1988"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB12","first-page":"451","article-title":"Hierarchical time stream Petri net: A model for hypermedia systems","volume":"935","author":"Senac","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB13","first-page":"139","article-title":"Tools and studies of formal techniques \u2014 Petri nets and temporal logic, Protocol Specification, Testing and Verification-III","author":"Antilla","year":"1983"},{"issue":"5","key":"10.1016\/S0140-3664(96)01158-9_BIB14","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1109\/12.24271","article-title":"Temporal Petri nets and their application to modeling and analysis of a Handshake Daisy Chain Arbiter","volume":"38","author":"Suzuki","year":"1989","journal-title":"IEEE Trans. Computers"},{"issue":"11","key":"10.1016\/S0140-3664(96)01158-9_BIB15","doi-asserted-by":"crossref","first-page":"1273","DOI":"10.1109\/32.60315","article-title":"Formal analysis of the alternating bit protocol by temporal Petri nets","volume":"16","author":"Suzuki","year":"1990","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"10.1016\/S0140-3664(96)01158-9_BIB16","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1109\/32.265633","article-title":"A new structural induction theorem for rings of temporal Petri nets","volume":"20","author":"Li","year":"1994","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/S0140-3664(96)01158-9_BIB17","first-page":"435","article-title":"Protocol analysis using numerical Petri nets","volume":"222","author":"Wheeler","year":"1985"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB18","first-page":"209","article-title":"A reduction theory for colored Petri nets","volume":"424","author":"Haddad","year":"1990"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB19","first-page":"278","article-title":"From colored Petri Nets to Object Petri nets","volume":"935","author":"Lakos","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB20","article-title":"Managing feature interactions in telephone systems by temporal colored Petri nets","author":"Cheung","year":"1996"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB21","first-page":"159","article-title":"Colored Petri nets extended with channels for synchronous communication","volume":"815","author":"Christensen","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB22","series-title":"Proc. IEEE Int. Conf. on Systems, Man and Cybernetics","first-page":"2245","article-title":"Detecting and resolving the interaction between telephone features Terminating Call Screening and Call Forwarding by colored Petri nets","author":"Cheung","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB23","first-page":"20","article-title":"OBJSA nets: a class of high-level nets having objects as domains","volume":"340","author":"Battiston","year":"1988"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB24","series-title":"16th Int. Conf. Applic. & Theory of Petri Nets","first-page":"31","article-title":"Modeling network protocols with Object Petri nets, Tutorial","author":"Lakos","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB25","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BFb0046845","article-title":"Transformations and decompositions of nets","volume":"254","author":"Berthelot","year":"1987","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB26","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/3-540-58152-9_20","article-title":"Liveness in bounded Petri nets which are covered by t-invariants","volume":"815","author":"Lautenbach","year":"1994","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB27","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1109\/TSMC.1987.4309041","article-title":"Generalized Petri net reduction methods","volume":"SMC-17","author":"Lee-Kwang","year":"1987","journal-title":"IEEE Trans. Systems, Man, Cybernetics"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB28","series-title":"Proc. SIGCOMM'86 Symp., Communications Architecture & Protocol","first-page":"305","article-title":"A Petri net reduction algorithm for protocol analysis","author":"Ramamoorthy","year":"1986"},{"issue":"5","key":"10.1016\/S0140-3664(96)01158-9_BIB29","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/32.286423","article-title":"Hierarchical reachability graph of bounded Petri nets for concurrent-software analysis","volume":"20","author":"Notomi","year":"1994","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/S0140-3664(96)01158-9_BIB30","article-title":"Equivalence transformations of Petri nets","volume":"424","author":"Hartmenn","year":"1990"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB31","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1016\/0743-7315(92)90010-K","article-title":"The application of EB-equivalence rules to the structural reduction of GSPN models","volume":"15","author":"Simone","year":"1992","journal-title":"J. Parallel and Distributed Computing"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB32","series-title":"10th Int. Conf. Applic. & Theory of Petri Nets","first-page":"1","article-title":"Stubborn sets for reduced state space generation","author":"Valmari","year":"1989"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB33","first-page":"397","article-title":"On-the-fly verification with stubborn sets","volume":"697","author":"Valmari","year":"1993"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB34","series-title":"Proc. 6th Ann. IEEE Symposium on Logic in Computer Science","first-page":"405","article-title":"A partial order approach to model checking","author":"Godefroid","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB35","first-page":"548","article-title":"On combining the stubborn set method with the sleep set method","volume":"815","author":"Varpaaniemi","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB36","first-page":"121","article-title":"An efficient algorithm for the computation of stubborn sets of well-formed Petri nets","volume":"935","author":"Brgan","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB37","first-page":"511","article-title":"Symbolic, symmetry, and stubborn set searches","volume":"815","author":"Tiusanen","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB38","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0022-0000(83)90029-6","article-title":"A method for stepwise refinement and abstraction of Petri nets","volume":"27","author":"Suzuki","year":"1983","journal-title":"J. Comp. System Sciences"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB39","article-title":"Behaviour preserving refinements of Petri nets","volume":"246","author":"Vogler","year":"1987"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB40","first-page":"277","article-title":"On liveness preservation by composition of nets via a set of places","volume":"524","author":"Souissi","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB41","series-title":"Design and Validation of Computer Protocols","author":"Holzmann","year":"1991"},{"issue":"4","key":"10.1016\/S0140-3664(96)01158-9_BIB42","doi-asserted-by":"crossref","DOI":"10.1109\/71.219756","article-title":"Dependency analysis \u2014 a Petri net based technique for synthesizing large concurrent systems","volume":"4","author":"Chen","year":"1993","journal-title":"IEEE Trans. Parallel and Distributed Systems"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB43","series-title":"Proc. 2nd Int. Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems","first-page":"325","article-title":"PN3-editor: Compositional Petri net editor for protocol specification","author":"Anisimov","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB44","first-page":"531","article-title":"Compositional analysis with place-bordered subnets","volume":"815","author":"Valmari","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB45","first-page":"377","article-title":"A client-server protocol for the composition of Petri nets","volume":"691","author":"Sibertin-Blanc","year":"1993"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB46","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/3-540-58152-9_26","article-title":"Cooperative nets","volume":"815","author":"Sibertin-Blanc","year":"1994","journal-title":"Lecture Notes in Computer Science"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB47","first-page":"342","article-title":"Colored Petri nets: A high level language for system design and analysis","volume":"483","author":"Jensen","year":"1990"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB48","article-title":"Invariant-preserving transformations for the verification of place\/transition systems (with application to communication protocols)","author":"Cheung","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB49","article-title":"Invariant-preserving transformations on colored Petri nets and their applications","author":"Cheung","year":"1996"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB50","series-title":"SDL '93: Using Objects","first-page":"179","article-title":"Towards a Petri net based semantics definition for message sequence charts","author":"Graubmann","year":"1993"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB51","year":"1992","journal-title":"CCITT Recommendation Z. 120"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB52","series-title":"2nd SDL Users and Implementors Forum","article-title":"A method and a tool for the validation of SDL-diagrams","author":"Graubmann","year":"1985"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB53","series-title":"SDL '91: Evolving Methods","article-title":"Towards an SDL-design-methodology using message sequence charts","author":"Grabowski","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB54","article-title":"Statische und dynamische analysen fur SDL-prozessgiagramme auf der basis von Petri-Netzen und sequence charts","author":"Grabowski","year":"1990"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB55","series-title":"Formal Description Techniques","first-page":"369","article-title":"Automatic translation of time Petri nets into ESTELLE description","author":"Alkhechi","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB56","series-title":"16th Int. Conf. Applic. & Theory of Petri Nets","first-page":"1","article-title":"Verification of SDL protocol specifications using Extended Petri nets, Tutorial","author":"Fischer","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB57","series-title":"16th Int. Conf. Applic. & Theory of Petri Nets","first-page":"13","article-title":"Analysis and verification of high-level-nets in combination with formal ESTELLE specifications, Tutorial","author":"Nutzel","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB58","first-page":"196","article-title":"On the relationship of CCS and Petri nets","volume":"172","author":"Golltz","year":"1984"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB59","first-page":"85","article-title":"An exercise in concurrency: A CSP process as a condition\/event system","volume":"340","author":"Degano","year":"1988"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB60","first-page":"196","article-title":"Operational Petri net semantics for CCSP","volume":"266","author":"Olderog","year":"1987"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB61","series-title":"Formal Description Techniques-I","first-page":"217","article-title":"Transformation from LOTOS to Galileo nets","author":"Marchena","year":"1989"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB62","first-page":"327","article-title":"TILT: from LOTOS to labelled transition systems","volume":"Vol. I","author":"Garavel","year":"1989"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB63","series-title":"Transactions of K.C. Wong Education Foundation Supported Lectures","first-page":"99","article-title":"A formal-method approach for cyclomatic complexity of distributed software","author":"Cheung","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB64","series-title":"16th Int. Conf. Applic. & Theory of Petri Nets","first-page":"19","article-title":"What is a correct test case? Elements of a Petri net oriented theory of protocol testing, Tutorial","author":"Baumgarten","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB65","first-page":"301","article-title":"Generating test sequences and their degrees of indeterminism for protocols, Protocol Specification, Testing and Verification-XI","author":"Cheung","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB66","series-title":"Proc. Int. Phoenix Conf. Computers and Communications","first-page":"245","article-title":"Executable selective test sequences with operational coverage for LOTOS specifications","author":"Cheung","year":"1993"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB67","series-title":"Proc. Software Education Conference","first-page":"42","article-title":"A tool for assessing the quality of distributed software designs specified in LOTOS","author":"Cheung","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB68","doi-asserted-by":"crossref","first-page":"940","DOI":"10.1006\/jpdc.1995.1091","article-title":"A fault-detection approach to conformance testing of nondeterministic distributed systems","volume":"28","author":"Cheung","year":"1995","journal-title":"J. Parallel and Distributed Computing"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB69","first-page":"304","article-title":"A survey of equivalence notions for net based systems","volume":"609","author":"Pomello","year":"1992"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB70","article-title":"A unified approach for equivalence relations of indeterministic distributed systems","author":"Wang","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB71","first-page":"432","article-title":"Functional equivalence of Petri nets","volume":"935","author":"Schreiber","year":"1995"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB72","series-title":"Proc. 4th International Workshop on Petri nets and Performance Models","article-title":"Modelling layered protocols in LOOPN","author":"Lakos","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB73","series-title":"Proc. 10th Euro. Conf. on Technology of Object-Oriented Languages and Systems","article-title":"Modelling a door controller protocol in LOOPN","author":"Lakos","year":"1993"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB74","first-page":"1","article-title":"An environment for object-oriented conceptual programming based on PROT nets","volume":"340","author":"Baldassari","year":"1988"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB75","series-title":"Proc. Int. Conf. Communications Technology (ICCT'92)","first-page":"15.11.1","article-title":"A Petri-Net-based synthesis algorithm for network protocol design","author":"Cheung","year":"1992"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB76","first-page":"118","article-title":"Top-down synthesis of live and bounded free choice nets","volume":"524","author":"Esparza","year":"1991"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB77","series-title":"Proc. 2nd Int. Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems","first-page":"234","article-title":"The knitting technique and its application to communication protocol synthesis","author":"Chao","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB78","first-page":"395","article-title":"From timed Petri nets to timed LOTOS","volume":"Vol X","author":"Bolognesi","year":"1990"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB79","series-title":"Feature Interactions in Telecommunications Systems","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB80","series-title":"Feature Interactions in Telecommunications Systems","first-page":"136","article-title":"Specifying features and analysing their interactions in a LOTOS environment","author":"Faci","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB81","unstructured":"W.M. Mak and T.Y. Cheung, Detecting feature interactions in the modular design of LOTOS specifications by temporal logic, Technical paper, Department of Computer Science, City University of Hong Kong, 19??"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB82","first-page":"386","article-title":"On the computation of structural synchronic invariants in P\/T nets","volume":"340","author":"Silva","year":"1988"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB83","first-page":"199","article-title":"New structural invariants for Petri nets analysis","volume":"815","author":"Couvreur","year":"1994"},{"key":"10.1016\/S0140-3664(96)01158-9_BIB84","first-page":"59","article-title":"Probabilistic validation of a remote call procedure","volume":"815","author":"Bennacer","year":"1994"}],"container-title":["Computer Communications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0140366496011589?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0140366496011589?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T08:25:13Z","timestamp":1556353513000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0140366496011589"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,12]]},"references-count":84,"journal-issue":{"issue":"14","published-print":{"date-parts":[[1996,12]]}},"alternative-id":["S0140366496011589"],"URL":"https:\/\/doi.org\/10.1016\/s0140-3664(96)01158-9","relation":{},"ISSN":["0140-3664"],"issn-type":[{"value":"0140-3664","type":"print"}],"subject":[],"published":{"date-parts":[[1996,12]]}}}