{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:31:45Z","timestamp":1672360305777},"reference-count":22,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[1993,2,1]],"date-time":"1993-02-01T00:00:00Z","timestamp":728524800000},"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":[[1993,2]]},"DOI":"10.1016\/0169-7552(93)90048-9","type":"journal-article","created":{"date-parts":[[2003,11,18]],"date-time":"2003-11-18T11:27:07Z","timestamp":1069154827000},"page":"779-790","source":"Crossref","is-referenced-by-count":25,"title":["VESAR: a pragmatic approach to formal specification and verification"],"prefix":"10.1016","volume":"25","author":[{"given":"B.","family":"Algayres","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V.","family":"Coelho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.","family":"Doldi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Garavel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Y.","family":"Lejeune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Rodr\u00edguez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0169-7552(93)90048-9_BIB1","series-title":"Formal Description Techniques","first-page":"85","article-title":"EWS\u2014an integrated workstation for the design and the automatic generation of distributed software","volume":"88","author":"Ayache","year":"1989"},{"key":"10.1016\/0169-7552(93)90048-9_BIB2","unstructured":"CCITT Red Book, Vol. VII.3 Recommendation T.70."},{"key":"10.1016\/0169-7552(93)90048-9_BIB3","series-title":"presented at 10th Annual Symposium on Principles of Programming Languages","first-page":"244","article-title":"Automatic verification of finite state concurrent systems using temporal logic","volume":"8","author":"Clarke","year":"1986"},{"key":"10.1016\/0169-7552(93)90048-9_BIB4","series-title":"Proc. IFIP WG6.1 7th International Symposium","article-title":"How could Estelle become a better FDT?","author":"Courtiat","year":"1987"},{"key":"10.1016\/0169-7552(93)90048-9_BIB5","series-title":"Proc. IFIP WG6.1 10th International Symposium","first-page":"359","article-title":"Compilation and verification of LOTOS specifications","author":"Garavel","year":"1990"},{"key":"10.1016\/0169-7552(93)90048-9_BIB6_1","series-title":"Proc. International Workshop on Automatic Verification Methods for Finite State Systems","article-title":"What are the limits of model-checking methods for the verification of real life protocols","author":"Graf","year":"1989"},{"key":"10.1016\/0169-7552(93)90048-9_BIB6_2","volume":"Vol. 407","author":"Graf","year":"1990"},{"key":"10.1016\/0169-7552(93)90048-9_BIB7","series-title":"Proc. IFIP WG6.1 6th International Workshop","article-title":"Unrestricted verification of protocol properties on a simulation: an observer approach","volume":"VI","author":"Groz","year":"1987"},{"key":"10.1016\/0169-7552(93)90048-9_BIB8","article-title":"V\u00e9rification des protocoles: l'ing\u00e9nierie des sp\u00e9cifications est en bonne voie","volume":"136","author":"Groz","year":"1989","journal-title":"l'Echo des Recherches"},{"key":"10.1016\/0169-7552(93)90048-9_BIB9_1","series-title":"Proc. International Workshop on Automatic Verification Methods for Finite State Systems","article-title":"Algorithms for automated protocol validation","author":"Holzmann","year":"1989"},{"key":"10.1016\/0169-7552(93)90048-9_BIB9_2","volume":"Vol. 407","author":"Holzmann","year":"1990"},{"key":"10.1016\/0169-7552(93)90048-9_BIB10","article-title":"Estelle\u2014A Formal Description Technique Based on an Extended State Transition Model","author":"ISO IS 9074","year":"1989","journal-title":"ISO\/IEC"},{"key":"10.1016\/0169-7552(93)90048-9_BIB11","article-title":"Deriving trace checkers for distributed systems","author":"Jard","year":"1987","journal-title":"Rapport de Recherche, INRIA No. 635"},{"key":"10.1016\/0169-7552(93)90048-9_BIB12_1","series-title":"Proc. International Workshop on Automatic Verification Methods for Finite State Systems","article-title":"On-line model checking for finite linear temporal logic specifications","author":"Jard","year":"1989"},{"key":"10.1016\/0169-7552(93)90048-9_BIB12_2","volume":"Vol. 407","author":"Jard","year":"1990"},{"key":"10.1016\/0169-7552(93)90048-9_BIB13","series-title":"Proc. IFIP WG6.1 9th International Symposium","article-title":"A multi-processor Estelle-to-C compiler to experiment distributed algorithms on parallel machines","volume":"IX","author":"Jard","year":"1990"},{"issue":"3","key":"10.1016\/0169-7552(93)90048-9_BIB14","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1109\/32.4654","article-title":"Development of VEDA: a prototyping tool for distributed algorithms","volume":"14","author":"Jard","year":"1988","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0169-7552(93)90048-9_BIB15","article-title":"Guider la simulation pour valider les protocoles","author":"Pageot","year":"1989","journal-title":"Th\u00e8se de Doctorat, Rennes"},{"key":"10.1016\/0169-7552(93)90048-9_BIB16","series-title":"Proc. 1st International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols\u2014FORTE 88","article-title":"Using Estelle for verification. An experience with the T70 teletex transport protocol","author":"Phalippou","year":"1989"},{"key":"10.1016\/0169-7552(93)90048-9_BIB17","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/BF00265555","article-title":"Fairness and related properties in transition systems\u2014a temporal logic to deal with fairness","volume":"19","author":"Queille","year":"1983","journal-title":"Acta Inform."},{"key":"10.1016\/0169-7552(93)90048-9_BIB18","series-title":"Proc. IFIP WG6.1 7th International Symposium","first-page":"235","article-title":"Verification in XESAR of the sliding window protocol","volume":"VII","author":"Richier","year":"1987"},{"key":"10.1016\/0169-7552(93)90048-9_BIB19","article-title":"Sp\u00e9cification et v\u00e9rification de syst\u00e8mes en XESAR","author":"Rodriguez","year":"1988","journal-title":"Th\u00e8se de Doctorat, Institut National Polytechnique de Grenoble"}],"container-title":["Computer Networks and ISDN Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0169755293900489?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0169755293900489?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T01:20:55Z","timestamp":1550366455000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0169755293900489"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,2]]},"references-count":22,"journal-issue":{"issue":"7","published-print":{"date-parts":[[1993,2]]}},"alternative-id":["0169755293900489"],"URL":"https:\/\/doi.org\/10.1016\/0169-7552(93)90048-9","relation":{},"ISSN":["0169-7552"],"issn-type":[{"value":"0169-7552","type":"print"}],"subject":[],"published":{"date-parts":[[1993,2]]}}}