{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:28:07Z","timestamp":1761596887861},"reference-count":23,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"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":3131,"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":[[2005,1]]},"DOI":"10.1016\/j.entcs.2004.12.009","type":"journal-article","created":{"date-parts":[[2005,1,9]],"date-time":"2005-01-09T04:55:22Z","timestamp":1105246522000},"page":"113-136","source":"Crossref","is-referenced-by-count":24,"special_numbering":"C","title":["ProTest: An Automatic Test Environment for B Specifications"],"prefix":"10.1016","volume":"111","author":[{"given":"Manoranjan","family":"Satpathy","sequence":"first","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Butler","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2004.12.009_bib001","series-title":"The B Book: Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"issue":"2","key":"10.1016\/j.entcs.2004.12.009_bib002","doi-asserted-by":"crossref","DOI":"10.1145\/356876.356879","article-title":"Validation, Verification and Testing of Computer Software","volume":"14","author":"Adrion","year":"1982","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/j.entcs.2004.12.009_bib003","unstructured":"Ambert, F., F. Bouquet, S. Chemin, S. Guenaud, B. Legeard, F. Peureux, N. Vacelet and M. Utting, BZ-TT: A Tool-Set for Test Generation from Z and B using Constraint Logic Programming, Formal Approaches to Testing of Software, Satellite Workshop of CONCUR02, August 24th, Brno, Czech Republic, 2002"},{"issue":"1","key":"10.1016\/j.entcs.2004.12.009_bib004","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1109\/32.825766","article-title":"Automatically Checking an Implementation against its Formal Specification","volume":"26","author":"Antoy","year":"2000","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/j.entcs.2004.12.009_bib005","unstructured":"Bernard, E., B. Legeard, X. Luck and F. Peureux, Generation of Test Sequences from Formal Specifications: GSM 11-11 Standard Case Study, Unpublished Draft"},{"key":"10.1016\/j.entcs.2004.12.009_bib006","series-title":"Black-Box Testing: Techniques for Functional Testing of Software and Systems","author":"Beizer","year":"1995"},{"key":"10.1016\/j.entcs.2004.12.009_bib007","series-title":"The PiLLoW Web Programming Library","author":"Cabeza","year":"2001"},{"key":"10.1016\/j.entcs.2004.12.009_bib008","author":"Canna"},{"key":"10.1016\/j.entcs.2004.12.009_bib009","series-title":"Proc. of the Eighth Z User Meeting","article-title":"A Tale of Two Paradigms: Formal Methods and Software Testing","author":"Carrington","year":"1994"},{"key":"10.1016\/j.entcs.2004.12.009_bib010","series-title":"Proc. of the FME'93: Industrial Strength Formal Methods Europe","first-page":"268","article-title":"Automating the generation and sequencing of test cases from modelbased specifications","volume":"670","author":"Dick","year":"1993"},{"key":"10.1016\/j.entcs.2004.12.009_bib011","article-title":"A note on two problems in connection with graphs","volume":"vol. 1","author":"Dijkstra","year":"1959"},{"key":"10.1016\/j.entcs.2004.12.009_bib012","series-title":"Graph Theory and its Applications","author":"Gross","year":"1999"},{"key":"10.1016\/j.entcs.2004.12.009_bib013","doi-asserted-by":"crossref","unstructured":"Hall, P.A.V., Relationship between Specifications and Testing, Information and Software Technology, Jan\/Feb 1991","DOI":"10.1016\/0950-5849(91)90023-5"},{"key":"10.1016\/j.entcs.2004.12.009_bib014","series-title":"Systematic Software Development using VDM","author":"Jones","year":"1990"},{"key":"10.1016\/j.entcs.2004.12.009_bib015","series-title":"Proc. of the FME'02 (Formal Methods Europe) Conference","first-page":"21","article-title":"Automated Boundary Testing from Z and B","volume":"No. 2391","author":"Legeard","year":"2002"},{"key":"10.1016\/j.entcs.2004.12.009_bib016","doi-asserted-by":"crossref","unstructured":"Leuschel, M., and M. Butler, ProB: A model-Checker for B, FM 2003: 12th International FME Symposium, Pisa, September 2003","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"10.1016\/j.entcs.2004.12.009_bib017","series-title":"Proc. of the 14th ICSE","first-page":"105","article-title":"Specification-based Test oracles for Reactive Systems","author":"Richardson","year":"1992"},{"key":"10.1016\/j.entcs.2004.12.009_bib018","unstructured":"Satpathy, M., R. Harrison, C. Snook, M. Butler, A Comparative Study of Formal and Informal Specifications through an Industrial Case Study, IEEE\/IFIP Joint Workshop on Formal Specifications of Computer Based Systems, Washington DC, April 2001"},{"key":"10.1016\/j.entcs.2004.12.009_bib019","unstructured":"Snook, C., and M. Butler, Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit. In UML 2000 Workshop on Dynamic Behaviour in UML Models: Semantic Questions, October 2000"},{"key":"10.1016\/j.entcs.2004.12.009_bib020","series-title":"Understanding Z","author":"Spivey","year":"1988"},{"issue":"11","key":"10.1016\/j.entcs.2004.12.009_bib021","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1109\/32.553698","article-title":"A Framework for Specification-Based Testing","volume":"22","author":"Stocks","year":"1996","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/j.entcs.2004.12.009_bib022","author":"Tatibouet"},{"issue":"4","key":"10.1016\/j.entcs.2004.12.009_bib023","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1093\/comjnl\/25.4.465","article-title":"On Testing Nontestable Programs","volume":"25","author":"Weyuker","year":"1982","journal-title":"The computer Journal"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104052351?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104052351?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T07:58:59Z","timestamp":1586073539000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104052351"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1]]},"references-count":23,"alternative-id":["S1571066104052351"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2004.12.009","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2005,1]]}}}