{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T06:41:07Z","timestamp":1698043267441},"reference-count":9,"publisher":"Wiley","issue":"5","license":[{"start":{"date-parts":[[2007,3,21]],"date-time":"2007-03-21T00:00:00Z","timestamp":1174435200000},"content-version":"vor","delay-in-days":6653,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems &amp;amp; Computers in Japan"],"published-print":{"date-parts":[[1989,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper describes the algebraic specification with a high degree of abstraction for the token ring LAN protocol provided in IEEE standard 802.5. Then the anticipated properties are verified by an algebraic method, the specification satisfies the safeness property (any frame transmitted from the active station either has been received by all stations or received by consecutive stations in the downstream without an error) and the mutual exclusion property (there exists one and only one token on the ring). The verification is carried out interactively using the verification support system. The process of selecting the lemmas to be introduced, the process of verification, CPU time used for the verification and the number of days needed in the verification are discussed.<\/jats:p>","DOI":"10.1002\/scj.4690200506","type":"journal-article","created":{"date-parts":[[2007,7,7]],"date-time":"2007-07-07T17:37:11Z","timestamp":1183829831000},"page":"57-68","source":"Crossref","is-referenced-by-count":0,"title":["Verification of safeness and mutual exclusion properties of algebraically specified token ring LAN protocol"],"prefix":"10.1002","volume":"20","author":[{"given":"Teruo","family":"Higashino","sequence":"first","affiliation":[]},{"given":"Mamoru","family":"Fujii","sequence":"additional","affiliation":[]},{"given":"Ken'Ichi","family":"Taniguchi","sequence":"additional","affiliation":[]},{"given":"Tadao","family":"Kasami","sequence":"additional","affiliation":[]},{"given":"Masaaki","family":"Mori","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2007,3,21]]},"reference":[{"key":"e_1_2_1_2_2","first-page":"177","volume-title":"Handbook for Software Eng","author":"Saito N.","year":"1986"},{"key":"e_1_2_1_3_2","first-page":"283","article-title":"Distributed processing and communication","volume":"19","author":"Noguchi S.","year":"1986","journal-title":"Computer Graphics"},{"issue":"7","key":"e_1_2_1_4_2","first-page":"773","article-title":"Verification of HDLC protocol by algebraic specification method","volume":"66","author":"Higashino T.","year":"1983","journal-title":"Trans. (D), I.E.C.E., Japan"},{"issue":"4","key":"e_1_2_1_5_2","first-page":"472","article-title":"Verification support system for algebraic specifications","volume":"67","author":"Higashino T.","year":"1984","journal-title":"Trans. (D), I.E.C.E., Japan"},{"key":"e_1_2_1_6_2","unstructured":"T.Higashino M.Higuchi K.Taniguchi T.Kasami M.Fujii andM.Mori.Automated verification of token ring LAN protocols. Proc. of the 1st Int. Conf. on Supercomputing Systems pp.361\u2013368(Dec.1985)."},{"issue":"5","key":"e_1_2_1_7_2","article-title":"Token Ring Access Method and Physical Layer Specifications","volume":"802","author":"IEEE Standards for Local Area Networks","year":"1985","journal-title":"IEEE Standard"},{"key":"e_1_2_1_8_2","unstructured":"M. Iri et al. (Ed.).Efficiency of computation and its limitation. Suppl. Math. Seminar Intr. Mod. Math. 13 Chapts. 4 5 (1980)."},{"key":"e_1_2_1_9_2","unstructured":"T.Sakata.Verification of safeness and mutual exclusion of token ring LAN with algebraic description. Spec. Rep. Dept. Inf. Eng. Fac. Eng. Sci. Osaka Univ. (March1986)."},{"key":"e_1_2_1_10_2","first-page":"93","volume-title":"Handbook for Software Eng","author":"Kasami T.","year":"1986"}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690200506","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690200506","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T12:59:16Z","timestamp":1697979556000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690200506"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,1]]},"references-count":9,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1989,1]]}},"alternative-id":["10.1002\/scj.4690200506"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690200506","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"value":"0882-1666","type":"print"},{"value":"1520-684X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,1]]}}}