{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:49:03Z","timestamp":1760586543788,"version":"3.28.0"},"reference-count":29,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,10]]},"DOI":"10.1109\/icsmc.2010.5641711","type":"proceedings-article","created":{"date-parts":[[2010,11,30]],"date-time":"2010-11-30T21:35:53Z","timestamp":1291152953000},"page":"2069-2074","source":"Crossref","is-referenced-by-count":22,"title":["Using task analytic models to visualize model checker counterexamples"],"prefix":"10.1109","author":[{"given":"Matthew L.","family":"Bolton","sequence":"first","affiliation":[]},{"given":"Ellen J.","family":"Bass","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.1998.725539"},{"key":"ref11","article-title":"The SAL language manual","author":"de moura","year":"2003","journal-title":"Technical Report CS-01–06"},{"article-title":"The cadence smv model checker","year":"0","author":"mcmillan","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-006-7999-y"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1570433.1570442"},{"article-title":"Towards an improved understanding of model-checking traces by visualisation","year":"2003","author":"kermelis","key":"ref15"},{"key":"ref16","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/3-540-45510-8_4","article-title":"UPPAAL - now, next, and future","author":"amnell","year":"2001","journal-title":"Proceedings of the 4th Summer School Modeling and Verification of Parallel Processes"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/32.54292"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"ref19","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/s10009-007-0047-9","article-title":"A framework for counterexample generation and exploration","volume":"9","author":"chechik","year":"2007","journal-title":"International Journal on Software Tools for Technology Transfer"},{"article-title":"smv2vcd","year":"2001","author":"tae jung kim","key":"ref28"},{"key":"ref4","doi-asserted-by":"crossref","DOI":"10.4324\/9781410605795","author":"schraagen","year":"2000","journal-title":"Cognitive Task Analysis"},{"article-title":"Verification of function block diagram through verilog translation","year":"2007","author":"jeon","key":"ref27"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1201\/b16826"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-010-0129-9"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-006-0008-8"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1518\/107118109X12524442637309"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2011.2109709"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2009.5346067"},{"article-title":"Using task analytic behavior modeling, erroneous human behavior generation, and formal methods to evaluate the role of human-automation interaction in system failure","year":"2010","author":"bolton","key":"ref2"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.1986.4308966"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"ref1"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2008.40"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2007.236"},{"key":"ref21","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-540-45069-6_22","article-title":"Evidence Explorer: A tool for exploring model-checking proofs","author":"dong","year":"2003","journal-title":"Proceedings of the 15th International Conference on Computer Aided Verification"},{"key":"ref24","article-title":"Automating model checking for autonomous systems","author":"simmons","year":"0","journal-title":"AAAI Spring Symposium on Real-Time Autonomous Systems"},{"key":"ref23","first-page":"6007","article-title":"Trace analysis-gain insight through modelchecking and cycle reduction","author":"kemper","year":"2006","journal-title":"Dortmund University of Technology Dortmund Tech Rep"},{"key":"ref26","first-page":"521","article-title":"MOCHA: Modularity in model checking","author":"alur","year":"1998","journal-title":"Proceedings of the 10th International Conference on Computer Aided Verification"},{"journal-title":"The SPIN Model Checker Primer and Reference Manual","year":"2003","author":"holzmann","key":"ref25"}],"event":{"name":"2010 IEEE International Conference on Systems, Man and Cybernetics - SMC","start":{"date-parts":[[2010,10,10]]},"location":"Istanbul, Turkey","end":{"date-parts":[[2010,10,13]]}},"container-title":["2010 IEEE International Conference on Systems, Man and Cybernetics"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5629466\/5641665\/05641711.pdf?arnumber=5641711","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T17:59:40Z","timestamp":1559843980000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5641711\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,10]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/icsmc.2010.5641711","relation":{},"subject":[],"published":{"date-parts":[[2010,10]]}}}