{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:39:51Z","timestamp":1725485991217},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540416630"},{"type":"electronic","value":"9783540446750"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44675-3_11","type":"book-chapter","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T20:44:02Z","timestamp":1180903442000},"page":"169-190","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formal Interactive Systems Analysis and Usability Inspection Methods: Two Incompatible Worlds?"],"prefix":"10.1007","author":[{"given":"Karsten","family":"Loer","sequence":"first","affiliation":[]},{"given":"Michael","family":"Harrison","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"J. Nielsen and R. L. Mack, Usability Inspection Methods, John Wiley & Sons, Inc. 1994","DOI":"10.1145\/259963.260531"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Virzi, R. A., Usability Inspection Methods, in Handbook of Human-Computer Interaction, K. Helander, Landauer T. K., and Prabhu P., Editors. 1997, chapter 29, Elsevier Science B. V.","DOI":"10.1016\/B978-044481862-1\/50095-9"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Harel, D., Statecharts: A visual formalism for complex systems. Science of Computer Programming, 1987: p. 231\u2013274.","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"McMillan, K. L., Symbolic model checking. 1993: Kluwer.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Norman, D. A., Design Principles for Human-Computer Interaction, in Proceedings of CHI\u201983. 1983, ACM. p. 1\u201310.","DOI":"10.1145\/800045.801571"},{"key":"11_CR6","volume-title":"Human Computer Interaction","author":"A. Dix","year":"1998","unstructured":"Dix, A., J. Finlay, G. Abowd, and R. Beale, Human Computer Interaction (2nd edition). 1998: Prentice Hall Europe.","edition":"2nd edition"},{"key":"11_CR7","unstructured":"Shneiderman, B., Designing the user interface: strategies for effective human-computerinteraction. 1998: Addison Wesley."},{"key":"11_CR8","first-page":"152","volume-title":"Proceedings of the CHI\u201994 Conf.","author":"J. Nielsen","year":"1994","unstructured":"Nielsen, J., Enhancing the explanatory power of usability heuristics, in Proceedings of the CHI\u201994 Conf. 1994, ACM: Boston, MA. p. 152\u2013158."},{"key":"11_CR9","first-page":"249","volume-title":"Proc. of ACM CHI\u201992 Conference on Human Factors in Computing Systems","author":"J. Nielsen","year":"1992","unstructured":"Nielsen, J. Finding usability problems through heuristic evaluation. in Proc. of ACM CHI\u201992 Conference on Human Factors in Computing Systems. pp249\u2013256. New York, 1992, ACM."},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"L\u00fcttgen, G. and V. Carre\u00f1o, Analyzing Mode Confusion via Model Checking. 1999, Technical Report, ICASE.","DOI":"10.1007\/3-540-48234-2_9"},{"key":"11_CR11","unstructured":"Rushby, J., Using Model Checking to Help Discover Mode Confusions and Other Automation Surprises, in (Pre-) Proceedings of the Workshop on Human Error, Safety, and System Development (HESSD). chapter 13, 1999."},{"key":"11_CR12","unstructured":"Palmer, E. Murphi busts an Altitude: A Murphi Analysis of an Automation Surprise. in Proceedings of the 18th Digital Avionics Systems Conference (DASC). 1999: IEEE Press."},{"key":"11_CR13","unstructured":"Butler, R. W., S. P. Miller, J. N. Potts, and V. A. Carre\u00f1o. A Formal Methods Approach to the Analysis of Mode Confusion. in Proceedings of the 17th Digital Avionics Systems Conference. 1998. Bellevue, Washington."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Abowd, G., H. Wang, and A. Monk, A formal technique for automated dialogue development, in Proceedings of the First Symposium on Designing Interactive Systems, DIS\u201995. 1995, ACM Press. p. 212\u2013226.","DOI":"10.1145\/225434.225459"},{"key":"11_CR15","volume-title":"A Method for Formal Specification and Verification of Interactive Systems","author":"F. D. Patern\u00f2","year":"1996","unstructured":"Patern\u00f2, F. D., A Method for Formal Specification and Verification of Interactive Systems. DPhil Thesis, Department of Computer Science, University of York, UK, 1996."},{"key":"11_CR16","volume-title":"Eurographics\u2019 90","author":"G. Faconti","year":"1990","unstructured":"Faconti, G. and F. Patern\u00f2. An approach to the formal presentation of the components of an interaction. in Eurographics\u2019 90. 1990. Montreaux: North-Holland."},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"d\u2019Ausbourg, B. Using Model Checking for the Automatic Validation of User Interfaces Systems. in P. Markopoulos and P. Johnson, eds., Design, Specification and Verification of Interactive Systems\u2019 98. 1998: Eurographics, Springer Verlag.","DOI":"10.1007\/978-3-7091-3693-5_16"},{"key":"11_CR18","volume-title":"Automated Deduction and Usability Reasoning","author":"J. C. Campos","year":"2000","unstructured":"Campos, J. C., Automated Deduction and Usability Reasoning. DPhil Thesis, Department of Computer Science, University of York, UK, 2000."},{"issue":"3","key":"11_CR19","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1111\/1467-8659.1230025","volume":"12","author":"D. J. Duke","year":"1993","unstructured":"Duke, D. J. and M. D. Harrison, Abstract Interaction Objects. Computer Graphics Forum, 1993. 12( 3): p. 25\u201336.","journal-title":"Computer Graphics Forum"},{"key":"11_CR20","unstructured":"Kyng, M., Creating Contexts for Design, in Scenario Based Design:Envisioning Work and Technology in System Development, J. M. Carroll, Editor. chapter 4, John Wiley & Sons, 1994."},{"key":"11_CR21","series-title":"Technical Report","volume-title":"THEA: Human Error Analysis for Requirements Definition","author":"B. Fields","year":"1997","unstructured":"Fields, B., M. D. Harrison, and P. Wright, THEA: Human Error Analysis for Requirements Definition. 1997, Technical Report YCS294, Department of Computer Science, University of York."},{"issue":"4","key":"11_CR22","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. M. Clarke","year":"1996","unstructured":"Clarke, E. M., J. M. Wing et al., Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 1996. 28(4): p. 626\u2013643.","journal-title":"ACM Computing Surveys"},{"key":"11_CR23","unstructured":"Degani, A., On Modes, Error, and Patterns of Interaction, PhD Thesis, Georgia Institute of Technology, 1996."},{"issue":"4","key":"11_CR24","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel, D., H. Loachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, A. Shtull-Trauring, and M. Trakhtenbrot, STATEMATE: A Working Environment for the Development od Complex Reactive Systems. IEEE Transactions on Software Engineering, 1990. 16(4): p. 403\u2013413.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR25","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0164-1212(97)00168-4","volume":"40","author":"J. M. Armstrong","year":"1998","unstructured":"Armstrong, J. M., Industrial Integration of Graphical and Formal Specifications. Journal of Systems & Software Special Issue on Formal Methods Technology Transfer, 1998. 40: p. 211\u2013225.","journal-title":"Journal of Systems & Software"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"von der Beeck, M., A Comparison of Statecharts Variants, in Formal Techniques in Real-Time and Fault-Tolerant Systems, H. Langmaack, W.-P. de Roever, and J. Vytopil, Editors. 1994, Springer-Verlag. p. 128\u2013148.","DOI":"10.1007\/3-540-58468-4_163"},{"issue":"4","key":"11_CR27","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D. Harel","year":"1996","unstructured":"Harel, D. and A. Namaad, The STATEMATE Semantics of Statecharts. ACM Transactions on Software Engineering and Methodology, 1996. 5(4): p. 293\u2013333.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"11_CR28","unstructured":"Loer, K. and Harrison, M., Model-checking statechart interface descriptions. 2000, in preparation."},{"key":"11_CR29","unstructured":"Mitchell, C. M., Operator Models, Model-Based Displays and Intelligent Aiding, in Human\/Technology in Complex Systems. 1996, JAI Press Inc. p. 67\u2013172."},{"key":"11_CR30","unstructured":"Kirwan, B., A Guide to Practical Human Reliability Assessment. 1994: Taylor & Francis."},{"key":"11_CR31","unstructured":"Campos, J. C. and M. D. Harrison. The role of verification in interactive system design. in P. Markopoulos and P. Johnson, eds., Design, Specification and Verification of Interactive Systems\u2019 98. 1998: Eurographics, Springer Verlag. p. 155\u2013170."},{"issue":"2","key":"11_CR32","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E. M., E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 1986. 8(2): p. 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Dwyer, M. B., G. S. Avrunin, and J. C. Corbett. Property Specification Patterns for Finite-State Verification. in M. Ardis, ed., 2nd Workshop on Formal Methods in Software Practice. 1998. p. 7\u201315.","DOI":"10.1145\/298595.298598"},{"key":"11_CR34","unstructured":"Dix, A., R. Mancini, and S. Levaldi, The cube \u2014 extending systems for undo, in Proceedings on the 4th Eurographics Workshop on Design, Specification and Verification of Interactive Systems (DSVIS), M. D. Harrison and J. C. Torres, Editors. 1997, Springer-Verlag. p. 119\u2013134."},{"key":"11_CR35","unstructured":"Butterworth, R., A. Blandford, and D. Duke. The role of formal proof in modelling interactive behaviour. in P. Markopoulos and P. Johnson, eds., Design, Specification and Verification of Interactive Systems\u2019 98. 1998: Eurographics, Springer Verlag p. 87\u2013101."}],"container-title":["Lecture Notes in Computer Science","Interactive Systems Design, Specification, and Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44675-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:38:18Z","timestamp":1558273098000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44675-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540416630","9783540446750"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-44675-3_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"11 May 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}