{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T18:30:30Z","timestamp":1683397830222},"reference-count":34,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2001,10,1]],"date-time":"2001-10-01T00:00:00Z","timestamp":1001894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4319,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,10]]},"DOI":"10.1016\/s1571-0661(04)00263-4","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T10:14:39Z","timestamp":1075371279000},"page":"370-381","source":"Crossref","is-referenced-by-count":6,"title":["Automated validation of distributed software using the IF environment"],"prefix":"10.1016","volume":"55","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Susanne","family":"Graf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Mounier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB1","unstructured":"Telelogic AB. SDT Reference Manual. http:\/\/www.telelogic.se\/."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB2","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing Abstractions of Infinite State Systems Compositionally and Automatically. In A. Hu and M. Vardi, editors, Proceedings of CAV'98 (Vancouver, Canada), volume 1427 of LNCS, pages 319\u2013331. Springer, June 1998.","DOI":"10.1007\/BFb0028755"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB3","doi-asserted-by":"crossref","unstructured":"S. Bornot, J. Sifakis, and S. Tripakis. Modeling Urgency in Timed Systems. In International Symposium: Compositionality - The Significant Difference (Holstein, Germany), volume 1536 of LNCS. Springer, September 1997.","DOI":"10.1007\/3-540-49213-5_5"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB4","doi-asserted-by":"crossref","unstructured":"D. Bo\u0161na\u010dki, D. Dams, L. Holenderski, and N. Sidorova. Model Checking SDL with Spin. In S. Graf and M. Schwartzbach, editors, Proceedings of TACAS'2000 (Berlin, Germany), volume 1785 of LNCS, pages 363\u2013377, Springer, March 2000.","DOI":"10.1007\/3-540-46419-0_25"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB5","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Cl. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for Branching Time Semantics. In Proceedings of ICALP'91, volume 510 of LNCS. Springer, July 1991.","DOI":"10.1007\/3-540-54233-7_126"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB6","doi-asserted-by":"crossref","unstructured":"M. Bozga, J. Cl. Fernandez, and L. Ghirvu. State Space Reduction based on Live Variables Analysis. In A. Cortesi and Fil\u00e9G., editors, Proceedings of SAS'99 (Venice, Italy), volume 1694 of LNCS, pages 164\u2013178. Springer, September 1999.","DOI":"10.1007\/3-540-48294-6_11"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB7","doi-asserted-by":"crossref","unstructured":"M. Bozga, J. Cl. Fernandez, and L. Ghirvu. Using Static Analysis to Improve Automatic Test Generation. In S. Graf and M. Schwartzbach, editors, Proceedings of TACAS'00 (Berlin, Germany), LNCS, pages 235\u2013250. Springer, March 2000.","DOI":"10.1007\/3-540-46419-0_17"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB8","doi-asserted-by":"crossref","unstructured":"M. Bozga, J.Cl. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, and L. Mounier. IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. In J.M. Wing, J. Woodcock, and J. Davies, editors, Proceedings of FM'99 (Toulouse, France), volume 1708 of LNCS, pages 307\u2013327. Springer, September 1999.","DOI":"10.1007\/3-540-48119-2_19"},{"issue":"1","key":"10.1016\/S1571-0661(04)00263-4_NEWBIB9","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S0167-6423(99)00017-9","article-title":"Verification and Test Generation for the SSCOP Protocol","volume":"36","author":"Bozga","year":"2000","journal-title":"Journal of Science of Computer Programming, Special Isssue on Formal Methods in Industry"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB10","doi-asserted-by":"crossref","unstructured":"M. Bozga, S. Graf, L. Mounier, I. Ober, J.L. Roux, and D. Vincent. Timed Extensions for SDL. In Proceedings of SDL FORUM'01, LNCS, 2001. to appear.","DOI":"10.1007\/3-540-48213-X_14"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB11","unstructured":"M. Bozga, D. Lesens, and L. Mounier. Model-Checking Ariane-5 Flight Program. In Proceedings of FMICS'01, 2001. to appear."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB12","doi-asserted-by":"crossref","unstructured":"J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting Finite-state Models from Java Source Code. In Proceedings of the 22nd International Conference on Software Engineering, June 2000.","DOI":"10.1145\/337180.337234"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB13","unstructured":"I. Dravapoulos, N. Pronios, and S. Denazis et al. The Magic WAND, Deliverable 3D5, Wireless ATM MAC, Final Report, August 1998."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB14","doi-asserted-by":"crossref","unstructured":"J.Cl. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A Protocol Validation and Verification Toolbox. In R. Alur and T.A. Henzinger, editors, Proceedings of CAV'96 (New Brunswick, USA), volume 1102 of LNCS, pages 437\u2013440. Springer, August 1996.","DOI":"10.1007\/3-540-61474-5_97"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB15","doi-asserted-by":"crossref","DOI":"10.1016\/S0167-6423(96)00032-9","article-title":"An Experiment in Automatic Generation of Test Suites for Protocols with Verification Technology","volume":"29","author":"Fernandez","year":"1997","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB16","doi-asserted-by":"crossref","unstructured":"H. Garavel. OPEN\/C\u00c6SAR: An Open Software Architecture for Verification, Simulation, and Testing. In B. Steffen, editor, Proceedings of TACAS'98 (Lisbon, Portugal), volume 1384 of LNCS, pages 68\u201384. Springer, March 1998.","DOI":"10.1007\/BFb0054165"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB17","unstructured":"S. Graf and G. Jia. Verification Experiments on the Mascara Protocol. In Proceedings of the SPIN'01 Workshop, 2001. to appear."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB18","doi-asserted-by":"crossref","unstructured":"S. Graf and B. Steffen. Compositional Minimisation of Finite State Processes. In E. Clarke and R. Kurshan, editors, Proceedings of CAV'90 (Rutgers, USA), volume 3 of DIMACS, pages 57\u201374. AMS\/ACM, 1990.","DOI":"10.1090\/dimacs\/003\/06"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB19","doi-asserted-by":"crossref","unstructured":"T.H. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A Model Checker for Hybrid Systems. In O. Grumberg, editor, Proceedings of CAV'97 (Haifa, Israel), volume 1254 of LNCS, pages 460\u2013463. Springer, June 1997.","DOI":"10.1007\/3-540-63166-6_48"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB20","unstructured":"Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall Software Series, http:\/\/cm.bell-labs.com\/cm\/cs\/what\/spin, 1991"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB21","unstructured":"HyPerformix. Ses\/Workbench. http:\/\/www.hyperformix.com\/."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB22","unstructured":"I-Logix. StateMate. http:\/\/www.ilogix.com\/."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB23","unstructured":"ISO\/IEC. LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Technical Report 8807, International Organization for Standardization \u2014 Information Processing Systems \u2014 Open Systems Interconnection, Gen\u00e8ve, 1988."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB24","unstructured":"ITU-T. Recommendation Q.2110. ATM Adaptation Layer \u2013 Service Specific Connection Oriented Protocol (SSCOP). Technical Report Q-2110, International Telecommunication Union \u2013 Standardization Sector, Gen\u00e8ve, 1994."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB25","unstructured":"ITU-T. Recommendation Z.100. Specification and Description Language (SDL). Technical Report Z-100, International Telecommunication Union \u2014 Standardization Sector, Gen\u00e8ve, November 1999."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB26","series-title":"Computer\u2013Aided Verification of Coordinating Processes: The Automata\u2013Theoretic Approach","author":"Kurshan","year":"1994"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB27","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, P. Petterson, and W. Yi. UPPAAL: Status & Developments. In O. Grumberg, editor, Proceedings of CAV'97 (Haifa, Israel), volume 1254 of LNCS, pages 456\u2013459. Springer, June 1997.","DOI":"10.1007\/3-540-63166-6_47"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB28","series-title":"Symbolic Model Checking: an Approach to the State Explosion Problem","author":"McMillan","year":"1993"},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB29","unstructured":"Inc MIL3. Optimized Network Engineering Tool OPNET. http:\/\/www.opnet.com\/."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB30","unstructured":"OMG. Unified Modeling Language Specification. Technical Report OMG UML v1.3 \u2014 ad\/99\u201306\u201309, Object Management Group, June 1999."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB31","unstructured":"Rational. Rational Rose. http:\/\/www.rational.com\/."},{"key":"10.1016\/S1571-0661(04)00263-4_NEWBIB32","unstructured":"Verilog. ObjectGEODE Reference Manual. http:\/\/www.verilogusa.com\/."},{"issue":"4","key":"10.1016\/S1571-0661(04)00263-4_NEWBIB33","doi-asserted-by":"crossref","DOI":"10.1109\/TSE.1984.5010248","article-title":"Program Slicing","volume":"SE-10","author":"Weiser","year":"1984","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1+2","key":"10.1016\/S1571-0661(04)00263-4_NEWBIB34","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","article-title":"KRONOS: A Verification Tool for Real-Time Systems","volume":"1","author":"Yovine","year":"1997","journal-title":"Software Tools for Technology Transfer"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002634?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104002634?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T12:26:18Z","timestamp":1585484778000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104002634"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,10]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2001,10]]}},"alternative-id":["S1571066104002634"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00263-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,10]]}}}