{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T23:40:12Z","timestamp":1758843612053,"version":"3.44.0"},"reference-count":13,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[1999,5,1]],"date-time":"1999-05-01T00:00:00Z","timestamp":925516800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1999,5,1]],"date-time":"1999-05-01T00:00:00Z","timestamp":925516800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2001,5,9]],"date-time":"2001-05-09T00:00:00Z","timestamp":989366400000},"content-version":"vor","delay-in-days":739,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Computer Communications"],"published-print":{"date-parts":[[1999,5]]},"DOI":"10.1016\/s0140-3664(99)00011-0","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:53:54Z","timestamp":1027594434000},"page":"681-690","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal verification and testing of protocols"],"prefix":"10.1016","volume":"22","author":[{"given":"D.R.","family":"Avresky","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0140-3664(99)00011-0_BIB1","doi-asserted-by":"crossref","unstructured":"D.R. Avresky, J. Arlat, J.C. Lapire, Y. Crouzet, Fault injection for the formal testing of fault tolerance, Proceedings of the Twenty-Second International Symposium of Fault-Tolerant Computing Systems (FTCS-22)-IEEE, Boston, MA, USA, July 8\u201310, 1992, pp. 345\u2013354.","DOI":"10.1109\/FTCS.1992.243566"},{"key":"10.1016\/S0140-3664(99)00011-0_BIB2","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1142\/S0218539394000155","article-title":"A multi-staged software design approach for fault tolerance","volume":"1","author":"Avresky","year":"1994","journal-title":"Int. J. of Reliability, Quality and Safety Engineering"},{"issue":"3","key":"10.1016\/S0140-3664(99)00011-0_BIB3","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1109\/24.537015","article-title":"Fault injection for the formal testing of fault tolerance","volume":"45","author":"Avresky","year":"1996","journal-title":"IEEE Trans. On Reliability"},{"key":"10.1016\/S0140-3664(99)00011-0_BIB4","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027047","article-title":"Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends","author":"Pnueli","year":"1986"},{"article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","year":"1981","author":"Clarke","key":"10.1016\/S0140-3664(99)00011-0_BIB5"},{"issue":"1","key":"10.1016\/S0140-3664(99)00011-0_BIB6","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"Sometimes and not never revisited: on branching versus linear time temporal logic","volume":"3","author":"Emerson","year":"1986","journal-title":"Journal of ACM"},{"key":"10.1016\/S0140-3664(99)00011-0_BIB7","unstructured":"E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, L.A. Ness, Verification of the Futurebus+Cache Coherence Protocol, Carnegie Mellon Univ. Technical Report, CMU-CS-92-206, 1992."},{"key":"10.1016\/S0140-3664(99)00011-0_BIB8","unstructured":"K.L. McMillan, J. Schwalbe, Formal Verification of the Encore Gigamax Cache Consistency Protocol, Proc. of the 1991 International Symposium on Shared Memory Multiprocessors, April 1991."},{"key":"10.1016\/S0140-3664(99)00011-0_BIB9","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1002\/spe.4380240805","article-title":"An interactive tool for design, simulation, verification and synthesis of protocols","volume":"24","author":"Chao","year":"1994","journal-title":"Software-Practice and Experience"},{"key":"10.1016\/S0140-3664(99)00011-0_BIB10","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/71.80145","article-title":"Deciding properties of timed transition models","volume":"1","author":"Ostroff","year":"1990","journal-title":"IEEE Trans. Parallel and Distributed Systems"},{"key":"10.1016\/S0140-3664(99)00011-0_BIB11","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1109\/32.387469","article-title":"Compiling real-time programs with timing constraint refinement and structural code motion","volume":"21","author":"Gerber","year":"1995","journal-title":"IEEE Trans. Software Engng."},{"issue":"5","key":"10.1016\/S0140-3664(99)00011-0_BIB12","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. Software Engng."},{"year":"1991","series-title":"Delta-4: A Generic Architecture for Dependable Distributed Computing","key":"10.1016\/S0140-3664(99)00011-0_BIB13"}],"container-title":["Computer Communications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0140366499000110?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0140366499000110?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T23:17:09Z","timestamp":1758842229000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0140366499000110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,5]]},"references-count":13,"journal-issue":{"issue":"7","published-print":{"date-parts":[[1999,5]]}},"alternative-id":["S0140366499000110"],"URL":"https:\/\/doi.org\/10.1016\/s0140-3664(99)00011-0","relation":{},"ISSN":["0140-3664"],"issn-type":[{"type":"print","value":"0140-3664"}],"subject":[],"published":{"date-parts":[[1999,5]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Formal verification and testing of protocols","name":"articletitle","label":"Article Title"},{"value":"Computer Communications","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S0140-3664(99)00011-0","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1999 Elsevier Science B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}