{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T22:30:22Z","timestamp":1693866622082},"reference-count":71,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1990,4,1]],"date-time":"1990-04-01T00:00:00Z","timestamp":638928000000},"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 Networks and ISDN Systems"],"published-print":{"date-parts":[[1990,4]]},"DOI":"10.1016\/0169-7552(90)90133-d","type":"journal-article","created":{"date-parts":[[2003,9,3]],"date-time":"2003-09-03T15:09:00Z","timestamp":1062601740000},"page":"185-201","source":"Crossref","is-referenced-by-count":16,"title":["Protocol verification for OSI"],"prefix":"10.1016","volume":"18","author":[{"given":"Bj\u00f6rn","family":"Pehrson","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0169-7552(90)90133-D_BIB1","doi-asserted-by":"crossref","DOI":"10.1109\/TSE.1987.232877","article-title":"SPANNER \u2014 A Tool for the Specification, Analysis, and Evaluation of Protocols","author":"Aggarwal","year":"1987","journal-title":"IEEE Trans. Software Engrg."},{"key":"10.1016\/0169-7552(90)90133-D_BIB2","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification III","article-title":"A Calculus for Protocol Specification, and Validation","author":"Aggarwal","year":"1984"},{"issue":"5","key":"10.1016\/0169-7552(90)90133-D_BIB3","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1145\/362946.362970","article-title":"A Note on Reliable Full-duplex Transmission over Half-duplex Links","volume":"12","author":"Bartlett","year":"1969","journal-title":"Comm. ACM"},{"key":"10.1016\/0169-7552(90)90133-D_BIB4","series-title":"Proc. ACM SIGCOMM","article-title":"Mechanical Verification and Automatic Implementation of Protocols","author":"Blumer","year":"1983"},{"key":"10.1016\/0169-7552(90)90133-D_BIB5","first-page":"361","article-title":"Finite State Description of Communication Protocols","volume":"2","author":"Bochmann","year":"1978","journal-title":"Comput. Networks"},{"key":"10.1016\/0169-7552(90)90133-D_BIB6","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VII","article-title":"Usage of Protocol Development Tools: The Results of A Survey","author":"Bochmann","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB7_1","series-title":"IFIP Int. Conf. on Protocol Specification, Testing and Verification VIII","article-title":"Specification of Protocols","author":"Bochmann","year":"1989"},{"key":"10.1016\/0169-7552(90)90133-D_BIB7_2","first-page":"167","volume":"18","year":"1989","journal-title":"Comput. Networks ISDN Systems"},{"issue":"4","key":"10.1016\/0169-7552(90)90133-D_BIB8","doi-asserted-by":"crossref","DOI":"10.1109\/TCOM.1980.1094685","article-title":"Formal Methods in Communication Protocol Design","volume":"28","author":"Bochmann","year":"1980","journal-title":"IEEE Trans. Comm."},{"key":"10.1016\/0169-7552(90)90133-D_BIB9","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VII","article-title":"Fundamental Results for the Verification of Observational Equivalence \u2014 A Survey","author":"Bolognesi","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB10","article-title":"SDL \u2014 System Description and Definition Language","author":"CCITT","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB11","series-title":"IFIP Int. Conf. on Protocol Specification, Testing and Verification III","article-title":"Automated Validation of Protocols using EDS","author":"Chung","year":"1988"},{"issue":"2","key":"10.1016\/0169-7552(90)90133-D_BIB12","doi-asserted-by":"crossref","DOI":"10.1145\/5397.5399","article-title":"Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM TOPLAS"},{"key":"10.1016\/0169-7552(90)90133-D_BIB13","series-title":"Proc. 6th Annual ACM Symp. on Principles of Distributed Systems","article-title":"Avoiding the State Explosion Problem in Temporal Logic Model Checking Algorithms","author":"Clarke","year":"1987"},{"key":"10.1016\/0169-7552(90)90133-D_BIB14","unstructured":"R. Cleveland, J. Parrow and B. Steffen, A. Semantic-Based Verification Tool for Finite-State Systems, in: Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification IX, Enschede (North-Holland, Amsterdam) to appear."},{"key":"10.1016\/0169-7552(90)90133-D_BIB15","series-title":"Proc. ACM SIGCOMM","article-title":"Petri Nets are Good for Protocols","author":"Courtiat","year":"1984"},{"key":"10.1016\/0169-7552(90)90133-D_BIB16","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification II","article-title":"Modeling and Analysis of Communication and Cooperation Protocols using Petri Net Based Models","author":"Diaz","year":"1982"},{"key":"10.1016\/0169-7552(90)90133-D_BIB17","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VIII","article-title":"A New Class of Analyzable CFSMs with Unbounded FIFO Channels","author":"Finkel","year":"1989"},{"key":"10.1016\/0169-7552(90)90133-D_BIB18","series-title":"Proc. Symp. in Applied Math. XIX","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning Meaning to Programs","author":"Floyd","year":"1967"},{"key":"10.1016\/0169-7552(90)90133-D_BIB19","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1016\/0169-7552(85)90086-8","article-title":"Protocol Validation by Fair Progress State Exploration","volume":"9","author":"Gouda","year":"1985","journal-title":"Comput. Networks ISDN Systems"},{"issue":"1","key":"10.1016\/0169-7552(90)90133-D_BIB20","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1109\/TCOM.1984.1095950","article-title":"Protocol Validation by Maximal Progress State Exploration","volume":"32","author":"Gouda","year":"1984","journal-title":"IEEE Trans. Comm."},{"key":"10.1016\/0169-7552(90)90133-D_BIB21","article-title":"Verifying Concurrent Processes Using Temporal Logic","volume":"129","author":"Hailpern","year":"1982"},{"issue":"1","key":"10.1016\/0169-7552(90)90133-D_BIB22","doi-asserted-by":"crossref","DOI":"10.1109\/TCOM.1983.1095720","article-title":"Modular Verification of Computer Communication Protocols","volume":"31","author":"Hailpern","year":"1983","journal-title":"IEEE Trans. Comm."},{"key":"10.1016\/0169-7552(90)90133-D_BIB23","series-title":"Data Communications, Computer Networks and OSI","author":"Halsall","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB24","series-title":"IEEE\/EUREL 8th European Conf. on Electrotechnics","article-title":"Specification and Validation of Services and Protocols for a Public Land Mobile ISDN System","author":"Hansson","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB25","series-title":"Algebraic Theory of Processes","author":"Hennessy","year":"1988"},{"issue":"1","key":"10.1016\/0169-7552(90)90133-D_BIB26","doi-asserted-by":"crossref","DOI":"10.1145\/2455.2460","article-title":"Algebraic Laws for Non-Determinism and Concurrency","volume":"32","author":"Hennessy","year":"1985","journal-title":"J. ACM"},{"issue":"10","key":"10.1016\/0169-7552(90)90133-D_BIB27","doi-asserted-by":"crossref","DOI":"10.1145\/363235.363259","article-title":"AN Axiomatic Basis for Computer Programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Comm. ACM"},{"key":"10.1016\/0169-7552(90)90133-D_BIB28","article-title":"Hennessy-Milner Logic with Recursion as a Specification Language and a Refinement Calculus Based on it","author":"Holmstr\u00f6m","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB29","series-title":"IFIP Int. Conf. on Protocol Specification, Testing and Verification VII","article-title":"On Limits and Possibilities of Automated Protocol Analysis","author":"Holzmann","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB30","unstructured":"ISO, The Reference Model of Open System Interconnection, ISO International Standard IS 7498."},{"key":"10.1016\/0169-7552(90)90133-D_BIB31","article-title":"Locaal Area Networks CSMA\/CD Access Method and Physical Layer Specification","author":"ISO","year":"1984","journal-title":"ISO\/TC97\/SC6"},{"key":"10.1016\/0169-7552(90)90133-D_BIB32","unstructured":"ISO, LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, ISO International Standard IS 8807."},{"key":"10.1016\/0169-7552(90)90133-D_BIB33","unstructured":"ISO, Estelle \u2014 A Formal Description Technique Based on an Extended State Transition Model, ISO International Standard IS 9074."},{"key":"10.1016\/0169-7552(90)90133-D_BIB34","series-title":"Proc. 6th Annual ACM Symp. on Principles of Distributed Systems","article-title":"Modular Verification of Asynchronous Networks","author":"Jonsson","year":"1987"},{"key":"10.1016\/0169-7552(90)90133-D_BIB35","article-title":"Towards a Knowledge Base for Design of (N) Service\/Protocol Pairs-An epistemic approach","author":"Juanole","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB36","series-title":"Proc. 9th FOCS","first-page":"58","article-title":"Some Theoretical Aspects of Applicative Multiprocessing","volume":"88","author":"Keller","year":"1980"},{"issue":"4","key":"10.1016\/0169-7552(90)90133-D_BIB37","first-page":"325","article-title":"Protocol Verification via projections","volume":"10","author":"Lam","year":"1984","journal-title":"IEEE Trans. Comm."},{"issue":"2","key":"10.1016\/0169-7552(90)90133-D_BIB38","doi-asserted-by":"crossref","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the Correctness of Multiprocess Programs","volume":"3","author":"Lamport","year":"1977","journal-title":"IEEE Trans. Software Engrg."},{"issue":"2","key":"10.1016\/0169-7552(90)90133-D_BIB39","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","article-title":"Specifying Concurrent Program Modules","volume":"5","author":"Lamport","year":"1983","journal-title":"ACM TOPLAS"},{"key":"10.1016\/0169-7552(90)90133-D_BIB40","article-title":"A Simple Approach to Specifying Concurrent Systems","author":"Lamport","year":"1986"},{"key":"10.1016\/0169-7552(90)90133-D_BIB41","article-title":"A Complete Protocol Verification using Relativized Bisimulation","author":"Larsen","year":"1986"},{"key":"10.1016\/0169-7552(90)90133-D_BIB42","series-title":"Proc. 12th ACM Symp. on Principles of Programming Languages","first-page":"97","article-title":"Checking that Finite State Concurrent Programs Satisfy Their Linear Specifications","author":"Lichtenstein","year":"1985"},{"issue":"5","key":"10.1016\/0169-7552(90)90133-D_BIB43","article-title":"Protocol Verification Using Reachability Analysis","volume":"17","author":"Lin","year":"1987","journal-title":"ACM SIGCOMM 1987, Comput. Comm. Rev."},{"key":"10.1016\/0169-7552(90)90133-D_BIB44","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/BF00288637","article-title":"An Axiomatic Approach to Total Correctness of Programs","volume":"3","author":"Manna","year":"1974","journal-title":"Acta Inform."},{"key":"10.1016\/0169-7552(90)90133-D_BIB45","series-title":"The Correctness Problem in Computer Science","first-page":"215","article-title":"The Temporal Framework for Concurrent Program","author":"Manna","year":"1981"},{"issue":"5","key":"10.1016\/0169-7552(90)90133-D_BIB46","article-title":"Algorithms for the Reduction of Timed Finite State Graphs","volume":"17","author":"Masapati","year":"1987","journal-title":"ACM SIGCOMM 1987, Comput. Comm. Rev."},{"key":"10.1016\/0169-7552(90)90133-D_BIB47","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VII","article-title":"Probabilistic Verification of Communication Protocols","author":"Maxemchuk","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB48","series-title":"Calculus for Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/0169-7552(90)90133-D_BIB49","series-title":"Proc. 6th Annual ACM Symp. on Principles of Distributed Systems","article-title":"Substituting for Real Time and Common Knowledge in Asynchronous Distributed Systems","author":"Neiger","year":"1987"},{"key":"10.1016\/0169-7552(90)90133-D_BIB50","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/BF01843567","article-title":"A Model and Temporal Proof System for Networks of Processes","volume":"1","author":"Nguyen","year":"1986","journal-title":"Distrib. Comput."},{"issue":"5","key":"10.1016\/0169-7552(90)90133-D_BIB51","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/360051.360224","article-title":"Verifying Properties of Parallel Programs","volume":"19","author":"Owicki","year":"1976","journal-title":"Comm. ACM"},{"issue":"3","key":"10.1016\/0169-7552(90)90133-D_BIB52","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","article-title":"Proving Liveness Properties of Concurrent Programs","volume":"4","author":"Owicki","year":"1982","journal-title":"ACM TOPLAS"},{"key":"10.1016\/0169-7552(90)90133-D_BIB53","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VII","article-title":"Protocol Description and Analysis Based on a State Transition Model with Channel Expressions","author":"Pachl","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB54","article-title":"Fairness Properties in Process Algebra","author":"Parrow","year":"1986"},{"key":"10.1016\/0169-7552(90)90133-D_BIB55","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VIII","article-title":"Verifying a CSMA\/CD-protocol with CCS","author":"Parrow","year":"1989"},{"key":"10.1016\/0169-7552(90)90133-D_BIB56","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VIII","article-title":"Tutorial on Verification of Protocols","author":"Pehrson","year":"1989"},{"issue":"1","key":"10.1016\/0169-7552(90)90133-D_BIB57","doi-asserted-by":"crossref","DOI":"10.1145\/42192.42195","article-title":"Specification and Verification of Liveness Properties of Cyclic, Concurrent Properties","volume":"10","author":"Reed","year":"1988","journal-title":"ACM TOPLAS"},{"key":"10.1016\/0169-7552(90)90133-D_BIB58","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VII","article-title":"Verification in Xesar of the Sliding Window Protocol","author":"Richier","year":"1988"},{"key":"10.1016\/0169-7552(90)90133-D_BIB59","first-page":"65","article-title":"An Improved Protocol Validation Technique","volume":"6","author":"Rubin","year":"1982","journal-title":"Comput. Networks"},{"key":"10.1016\/0169-7552(90)90133-D_BIB60","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification III","article-title":"From Formal Protocol Specification Towards Automated Performance Prediction","author":"Rudin","year":"1983"},{"key":"10.1016\/0169-7552(90)90133-D_BIB61","doi-asserted-by":"crossref","first-page":"924","DOI":"10.1109\/26.3772","article-title":"An Algorithmic Technique for Protocol Verification","author":"Sabnani","year":"1988","journal-title":"IEEE Trans. Comm."},{"key":"10.1016\/0169-7552(90)90133-D_BIB62","doi-asserted-by":"crossref","DOI":"10.1109\/TCOM.1982.1095451","article-title":"From State Machines to Temporal Logic: Specification Methods for Protocol Standards","author":"Schwartz","year":"1982","journal-title":"IEEE Trans. Comm."},{"issue":"4","key":"10.1016\/0169-7552(90)90133-D_BIB63","doi-asserted-by":"crossref","DOI":"10.1145\/357377.357384","article-title":"An HDLC Protocol Specification and Its Verification Using Image Protocols","volume":"1","author":"Shankar","year":"1983","journal-title":"ACM TOCS"},{"key":"10.1016\/0169-7552(90)90133-D_BIB64","series-title":"Proc. TAPSOFT 1989","first-page":"369","article-title":"Local Model Checking in the Modal Mu-calculus","volume":"351","author":"Stirling","year":"1989"},{"key":"10.1016\/0169-7552(90)90133-D_BIB65","series-title":"Proc. IEEE Symp. on Logic in Computer Science","article-title":"An Automata-Theoretic Approach to Automatic Program Verification","author":"Vardi","year":"1986"},{"key":"10.1016\/0169-7552(90)90133-D_BIB66","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification V","article-title":"The Importance of the Service Concept in the Design of Data Communication Protocols","author":"Vissers","year":"1986"},{"key":"10.1016\/0169-7552(90)90133-D_BIB67","series-title":"Proc. IFIP Int. Conf. on Protocol Specification, Testing and Verification VI","article-title":"Protocol Validation by Random State Exploration","author":"West","year":"1987"},{"key":"10.1016\/0169-7552(90)90133-D_BIB68","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1147\/rd.221.0060","article-title":"Automated Validation of a Communication Protocol: The CCITT X.21 Recommendation","volume":"2","author":"West","year":"1978","journal-title":"IBM J. Res. Develop."},{"issue":"4","key":"10.1016\/0169-7552(90)90133-D_BIB69","doi-asserted-by":"crossref","DOI":"10.1109\/TCOM.1980.1094687","article-title":"Towards Analyzing and Synthesizing Protocols","volume":"28","author":"Zafiropulo","year":"1980","journal-title":"IEEE Trans. Comm."},{"issue":"5","key":"10.1016\/0169-7552(90)90133-D_BIB70","article-title":"Extension to Communicating Sequential Processes to Allow Protocol Performance Specification","volume":"17","author":"Zic","year":"1987","journal-title":"ACM SIGCOMM 1987, Comput. Comm. Rev."}],"container-title":["Computer Networks and ISDN Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016975529090133D?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:016975529090133D?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T12:54:07Z","timestamp":1551099247000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/016975529090133D"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,4]]},"references-count":71,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1990,4]]}},"alternative-id":["016975529090133D"],"URL":"https:\/\/doi.org\/10.1016\/0169-7552(90)90133-d","relation":{},"ISSN":["0169-7552"],"issn-type":[{"value":"0169-7552","type":"print"}],"subject":[],"published":{"date-parts":[[1990,4]]}}}