{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T13:37:03Z","timestamp":1777901823249,"version":"3.51.4"},"reference-count":12,"publisher":"SAGE Publications","issue":"5","license":[{"start":{"date-parts":[[1995,11,1]],"date-time":"1995-11-01T00:00:00Z","timestamp":815184000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIMULATION"],"published-print":{"date-parts":[[1995,11]]},"abstract":"<jats:p>This paper describes the technique of simulating and verifying communication protocols using a computer-aided tool, called Deductive Machine, which implements some verification theories that are based on Deductive Systems. The merit of using Deductive Machine is that it simulates the execution of a protocol and at the same time verifies the protocol against certain properties by observing the outcome of the execution. By simply adding one or more new rules concerning the new situations, conducting the simulation exercise again and checking the outcomes against some protocol verification theories, one can conclude whether the protocol still works well under the new conditions. Simulation and verification of a protocol can thus be performed in an incremental manner. The results of using the Deductive Machine to simulate and verify the extended alternating bit protocol, with real life conditions taken into consideration, are reported in this paper in order to demonstrate the usefulness of the tool and the viability of this technique to simulate and verify complex communication protocols.<\/jats:p>","DOI":"10.1177\/003754979506500505","type":"journal-article","created":{"date-parts":[[2007,3,18]],"date-time":"2007-03-18T03:46:49Z","timestamp":1174189609000},"page":"321-333","source":"Crossref","is-referenced-by-count":2,"title":["Simulation and Verification of Protocol Using Deductive Machine"],"prefix":"10.1177","volume":"65","author":[{"given":"R.","family":"Lai","sequence":"first","affiliation":[{"name":"Department of Computer Science and Computer Engineering La Trobe University Victoria, Australia 3083"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"X.","family":"Li","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Computer Engineering La Trobe University Victoria, Australia 3083"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[1995,11,1]]},"reference":[{"key":"atypb1","volume-title":"Proceedings of the Workshop on Protocol Specification, Testing, and Verification. IV, Skylodge","author":"Bolognesi, T."},{"key":"atypb2","volume-title":"Proceedings of Fourth International Conference on Formal Description Techniques","author":"Hansson, H."},{"key":"atypb3","volume-title":"Proceedings of the 4th International Conference on Computing and Information","author":"Li, X."},{"key":"atypb4","volume-title":"Proceedings of the 5th International Conference on Computing and Information","author":"Li, X."},{"key":"atypb5","volume-title":"Proceedings of the Singapore International Conference on Networks and International Conference on Information Engineering '93","author":"Li, X."},{"key":"atypb6","volume-title":"Petri Net Theory and Modelling of Systems","author":"Peterson, J.","year":"1981"},{"key":"atypb7","volume-title":"Verification Results for ISO FTAM Basic Protocol","author":"Lai, R.","year":"1989"},{"key":"atypb8","volume-title":"Theory of Deductive Systems and Its Applications","author":"Maslov, S. Yu.","year":"1987"},{"key":"atypb9","volume-title":"Introduction to Mathematical Logic","author":"Mendelson, E.","year":"1979"},{"key":"atypb10","author":"Post, E.L.","year":"1943","journal-title":"American Journal of Mathematics"},{"key":"atypb11","doi-asserted-by":"publisher","DOI":"10.1109\/32.4651"},{"key":"atypb12","volume-title":"VALIRA- A Tool for Protocol Validation via Reachability Analysis","author":"Vuong, S.T.","year":"1987"}],"container-title":["SIMULATION"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/003754979506500505","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/003754979506500505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:10:34Z","timestamp":1777633834000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/003754979506500505"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,11]]},"references-count":12,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1995,11]]}},"alternative-id":["10.1177\/003754979506500505"],"URL":"https:\/\/doi.org\/10.1177\/003754979506500505","relation":{},"ISSN":["0037-5497","1741-3133"],"issn-type":[{"value":"0037-5497","type":"print"},{"value":"1741-3133","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,11]]}}}