{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T20:43:44Z","timestamp":1698007424451},"reference-count":9,"publisher":"Wiley","issue":"9","license":[{"start":{"date-parts":[[2007,3,21]],"date-time":"2007-03-21T00:00:00Z","timestamp":1174435200000},"content-version":"vor","delay-in-days":7384,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems &amp; Computers in Japan"],"published-print":{"date-parts":[[1987,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper considers the communication protocol whose specification is described algebraically in a style of an \u201cabstract sequential machine.\u201d A method is presented to verify the progress property of the protocol, such that the transmitted data will eventually be received. First, by the algebraic method, we verify some static properties (invariants) which hold in any state reachable by the execution of the state transitions permitted by the protocol. Also, we verify the relations which hold between the states before and after the execution of each state transition. These relations are transformed into the formulas of the temporal logic by using some transformation rules. At the same time, the formulas of the temporal logic are provided as the assumptions for the stations and communication lines, which are needed in the discussion of progress property of the protocol, such that the communication lines are not functionally cut off. Using these formulas and standard axioms in the temporal logic (inference rules), it is shown that the predicates representing the progress property of the protocol are true. The foregoing is the outline of the discussions in this paper. This paper applies the method to Stenning's data transfer protocol, and the progress property is verified.<\/jats:p>","DOI":"10.1002\/scj.4690180910","type":"journal-article","created":{"date-parts":[[2007,7,7]],"date-time":"2007-07-07T14:22:12Z","timestamp":1183818132000},"page":"96-107","source":"Crossref","is-referenced-by-count":0,"title":["Verification of progress property of algebraically specified communication protocols"],"prefix":"10.1002","volume":"18","author":[{"given":"Teruo","family":"Higashino","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ken'Ichi","family":"Taniguchi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tadao","family":"Kasami","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mamoru","family":"Fujii","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masaaki","family":"Mori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2007,3,21]]},"reference":[{"issue":"2","key":"e_1_2_1_2_2","first-page":"187","article-title":"Formal description techniques for protocol","volume":"68","author":"Kawaoka","year":"1985","journal-title":"Proc. I. E. C. E., Japan"},{"key":"e_1_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0376-5075(76)90015-5"},{"key":"e_1_2_1_4_2","first-page":"324","article-title":"A specification defined as an extension of a base algebra","volume":"64","author":"Sugiyama Y.","year":"1981","journal-title":"Trans. (D) I. E. C. E., Japan"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010311"},{"key":"e_1_2_1_6_2","article-title":"Algebraic specification of Stenning's data transfer protocol and its verification","volume":"83","author":"Kudo T.","year":"1984","journal-title":"Tech. Rep. I. E. C. E., Japan"},{"key":"e_1_2_1_7_2","unstructured":"T.Higushino K.Taniguchi Nawata Y.SugiyamaandT.Kasami.Verification of progress properties of an algebraic specification of Stenning's data transfer protocol Proc. LA Symp. pp.102\u2013111(July1985)."},{"issue":"4","key":"e_1_2_1_8_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_9_2","volume-title":"Lecture Notes in Computer Science 129","author":"Hailpern B. T.","year":"1982"},{"key":"e_1_2_1_10_2","unstructured":"B. T.HailpernandS.Owicki.Verifying Network Protocols Using Temporal Logic Proceedings of Trends and Applications 1980 I. E. E. E. Computer Society pp.18\u201328(1980)."}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690180910","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690180910","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,21]],"date-time":"2023-10-21T06:41:49Z","timestamp":1697870509000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690180910"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,1]]},"references-count":9,"journal-issue":{"issue":"9","published-print":{"date-parts":[[1987,1]]}},"alternative-id":["10.1002\/scj.4690180910"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690180910","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"value":"0882-1666","type":"print"},{"value":"1520-684X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1987,1]]}}}