{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:08:27Z","timestamp":1759032507743},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,6,1]],"date-time":"1993-06-01T00:00:00Z","timestamp":738892800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,6]]},"DOI":"10.1007\/bf01384135","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T06:04:39Z","timestamp":1112421879000},"page":"277-321","source":"Crossref","is-referenced-by-count":5,"title":["Test case verification by model checking"],"prefix":"10.1007","volume":"2","author":[{"given":"Kshirasagar","family":"Naik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Behcet","family":"Sarikaya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"K. Naik and B. Sarikaya Testing communication protocols.IEEE Software, 27?37, 1992","DOI":"10.1109\/52.108777"},{"key":"CR2","unstructured":"ISO\/IEC 9646: Information Technology-Open Systems Interconnection-Conformance Testing Methodology and Framework, 1991."},{"key":"CR3","unstructured":"ISO\/IEC IS8807: LOTOS, a formal description technique based on the temporal ordering of observable behavior, ISO\/TC97\/SC21\/WG1-FDT\/SC-C, June 1988."},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"T. Bolognesi and E. Brinksma. Introduction to ISO specification language LOTOS.Computer Networks and ISDN Systems, 25?59 1987.","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"CR5","unstructured":"ISO\/IEC IS9074: Estelle ? A formal description technique based on an extended state transition model, ISO\/TC97\/SC21\/WG1, 1987."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0169-7552(87)90084-5","volume":"14","author":"S. Budkowski","year":"1987","unstructured":"S. Budkowski and P. Dembinski. An introduction to Estelle: A specification language for distributed systems.Computer Networks and ISDN Systems, 14: 3?23, 1987.","journal-title":"Computer Networks and ISDN Systems"},{"key":"CR7","unstructured":"CCITT, Specification and Description Language SDL, Recommendation Z.100, 1992."},{"key":"CR8","unstructured":"ISO\/IEC 8824: Profile of abstract syntax notation one, IS8824, 1987."},{"issue":"4","key":"CR9","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1109\/32.16602","volume":"15","author":"D.P. Sidhu","year":"1989","unstructured":"D.P. Sidhu and T.K. Leung. Formal methods for protocol testing: A detailed study.IEEE Trans. on Software Engineering, 15 (4): 413?426, 1989.","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"8","key":"CR10","doi-asserted-by":"crossref","first-page":"1317","DOI":"10.1109\/5.58319","volume":"78","author":"A.T. Dahbura","year":"1990","unstructured":"A.T. Dahbura, T.K. Sabnani, and M.U. Uyar. Formal methods for generating protocol conformance test sequencesProceedings of the IEEE, 78 (8): 1317?1326, 1990.","journal-title":"Proceedings of the IEEE"},{"issue":"5","key":"CR11","doi-asserted-by":"crossref","first-page":"518","DOI":"10.1109\/TSE.1987.233197","volume":"13","author":"B. Sarikaya","year":"1989","unstructured":"B. Sarikaya, G.v. Bochmann, E. Cerny. A test design methodology for protocol testing.IEEE Trans. on Software Eng., 13(5): 518?526, 1989.","journal-title":"IEEE Trans. on Software Eng."},{"key":"CR12","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1109\/12.88472","volume":"40","author":"P. Tripathy","year":"1991","unstructured":"P. Tripathy and B. Sarikaya. Test case generation from LOTOS specification.IEEE Trans. on Computers, 40: 543?552, 1991.","journal-title":"IEEE Trans. on Computers"},{"key":"CR13","unstructured":"Abstract test suite for transport protocol class 2. The National Computing Centre Limited, Manchester, UK, 1988."},{"issue":"2","key":"CR14","first-page":"20","volume":"1","author":"J.B. Goodenough","year":"1975","unstructured":"J.B. Goodenough and S.L. Gerhart. Toward a theory of test data selection.IEEE Trans. on Sofware Eng., SE-1 (2): 20?37, 1975.","journal-title":"IEEE Trans. on Sofware Eng., SE"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0169-7552(89)90004-4","volume":"17","author":"B. Sarikaya","year":"1989","unstructured":"B. Sarikaya. Conformance testing: Architectures and test sequences.Computer Networks and ISDN Systems, 17: 111?126, 1989.","journal-title":"Computer Networks and ISDN Systems"},{"issue":"2","key":"CR16","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"D. Brand and P. Zafiropulo. On communicating finite-state machines.JACM 30, (2): 323?342, 1983.","journal-title":"JACM"},{"key":"CR17","unstructured":"K. Naik and B. Sarikaya. An extended finite state machine model for TTCN. Proc. of the 15th. Biennial Symposium on Communications, Kingston, Ontario, 1990, pp. 296?299."},{"key":"CR18","unstructured":"Information Processing Systems-Open System Interconnection-Basic Reference Model, ISO 7498, 1984."},{"key":"CR19","unstructured":"M. Jackson.System development. Prentice Hall, 1983."},{"key":"CR20","volume-title":"Verification of test cases for protocol conformance testing","author":"K. Naik","year":"1992","unstructured":"K. Naik.Verification of test cases for protocol conformance testing. Ph.D. theseis, Concordia University, Montreal, 1992."},{"key":"CR21","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1109\/TC.1982.1675978","volume":"31","author":"G. Bochmann v.","year":"1982","unstructured":"G. v. Bochmann. Hardware specification with temporal logic: An example.IEEE Trans. on Computers, C-31: 223?231, 1982.","journal-title":"IEEE Trans. on Computers, C"},{"issue":"2","key":"CR22","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules.ACM TOPLAS, 5, (2): 190?222, 1983.","journal-title":"ACM TOPLAS"},{"issue":"2","key":"CR23","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications.ACM TOPLAS, 8 (2), 224?263, 1986.","journal-title":"ACM TOPLAS"},{"issue":"8","key":"CR24","doi-asserted-by":"crossref","first-page":"924","DOI":"10.1109\/26.3772","volume":"36","author":"K. Sabnani","year":"1988","unstructured":"K. Sabnani, An algorithm technique for protocol verification.IEEE Transaction on Comm, COM-36 (8): 924?931, 1988.","journal-title":"IEEE Transaction on Comm, COM"},{"key":"CR25","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"M. Ben-Ari. A. Pnueli, and Z. Manna. The temporal logic of branching time.Acta Informatica, 20: 207?225, 1983.","journal-title":"Acta Informatica"},{"key":"CR26","unstructured":"J.C. Fernandez, J.L. Richier, and J. Voiron. Verification of protocol specifications using the CESAR system. IFIP PSTV V, 1985."},{"key":"CR27","volume-title":"A Unified Model for test generation for communication protocols","author":"P. Tripathy","year":"1992","unstructured":"P. Tripathy.A Unified Model for test generation for communication protocols. Ph.D. thesis, Concordia University, Montreal, 1992."},{"issue":"4","key":"CR28","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1147\/rd.224.0393","volume":"22","author":"C.H. West","year":"1978","unstructured":"C.H. West. General techniques for communication protocol validation.IBM Journal of Res. and Development, 22 (4): 393?404, 1978.","journal-title":"IBM Journal of Res. and Development"},{"key":"CR29","first-page":"65","volume":"6","author":"J. Rubin","year":"1982","unstructured":"J. Rubin and C.H. West. An improved protocol validation technique.Computer Networks, 6: 65?73, 1982.","journal-title":"Computer Networks"},{"issue":"4","key":"CR30","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1109\/TCOM.1980.1094687","volume":"28","author":"P. Zafiropulo","year":"1980","unstructured":"P. Zafiropulo, C.H. West, H. Rudin, D.D. Cowan, and D. Brand. Towards analyzing and synthesizing protocols.IEEE Trans. on Comm., COM-28 (4): 651?661, 1980.","journal-title":"IEEE Trans. on Comm., COM"},{"issue":"4","key":"CR31","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1109\/TCOM.1984.1096074","volume":"32","author":"B. Sarikaya","year":"1984","unstructured":"B. Sarikaya and G. v. Bochmann. Synchronization and specification issues in protocol testing.IEEE Trans. on Comm. COM-32 (4): 389?395, 1984.","journal-title":"IEEE Trans. on Comm. COM"},{"key":"CR32","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0169-7552(90)90121-8","volume":"18","author":"G. Bochmann v.","year":"1990","unstructured":"G. v. Bochmann. Specification of a simplified transport protocol using different formal description techniques.Computer and Networks and ISDN Systems, 18: 335?377, 1990.","journal-title":"Computer and Networks and ISDN Systems"},{"key":"CR33","unstructured":"M. Dubuc and G. v. Bochmann. Translation from TTCN to LOTOS and verification of Test Cases.FORTE'90, Madrid, 1990."},{"key":"CR34","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0164-1212(92)90018-F","volume":"19","author":"K. Naik","year":"1992","unstructured":"K. Naik and B. Sarikaya. Verification of protocol conformance test cases using reachability analysis.The Journal of Systems Sofware, 19: 41?57, 1992.","journal-title":"The Journal of Systems Sofware"},{"key":"CR35","doi-asserted-by":"crossref","unstructured":"U. Bar and J.M. Schneider. Automated validation of TTCN test suites. IFIP PSTV XII, Orlando, FL, pp. 279?295, 1992.","DOI":"10.1016\/B978-0-444-89874-6.50024-6"},{"key":"CR36","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1002\/spe.4380180406","volume":"18","author":"L. Logrippo","year":"1988","unstructured":"L. Logrippo, et al. An interpreter for LOTOS, A specification language for distributed systems.Software Practice and Experience, 18: 365?385, 1988.","journal-title":"Software Practice and Experience"},{"key":"CR37","doi-asserted-by":"crossref","unstructured":"F.J. Lin, P.M. Chu, and M.T. Liu. Protocol verification using reachability analysis: The state space explosion problem and relief strategies. SIGCOMM'87, Stowe, Vermont, 126?135, 1987.","DOI":"10.1145\/55483.55496"},{"issue":"2","key":"CR38","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/71.80145","volume":"1","author":"J.S. Ostroff","year":"1990","unstructured":"J.S. Ostroff. Deciding properties of timed transition models.IEEE Trans. on Parallel and Distributed Systems 1 (2): 170?183, 1990.","journal-title":"IEEE Trans. on Parallel and Distributed Systems"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384135.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384135\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384135","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:29:58Z","timestamp":1586190598000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,6]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,6]]}},"alternative-id":["BF01384135"],"URL":"https:\/\/doi.org\/10.1007\/bf01384135","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,6]]}}}