{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T14:04:25Z","timestamp":1771509865516,"version":"3.50.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2001,8,1]],"date-time":"2001-08-01T00:00:00Z","timestamp":996624000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,8,1]],"date-time":"2001-08-01T00:00:00Z","timestamp":996624000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Automated Software Engineering"],"published-print":{"date-parts":[[2001,8]]},"DOI":"10.1023\/a:1011265604021","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T09:18:21Z","timestamp":1040635101000},"page":"275-310","source":"Crossref","is-referenced-by-count":53,"title":["Model Checking Interactor Specifications"],"prefix":"10.1007","volume":"8","author":[{"given":"Jos\u00e9 C.","family":"Campos","sequence":"first","affiliation":[]},{"given":"Michael D.","family":"Harrison","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"337710_CR1","doi-asserted-by":"crossref","unstructured":"Abowd, G.D., Wang, H.\u2013M., and Monk, A.F. 1995. A formal technique for automated dialogue development. In Proceedings of the First Symposium of Designing Interactive Systems\u2014DIS'95, ACM Press, pp. 219\u2013226.","DOI":"10.1145\/225434.225459"},{"issue":"1","key":"337710_CR2","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/32.210305","volume":"19","author":"J.M. Atlee","year":"1993","unstructured":"Atlee, J.M. and Gannon, J. 1993. State\u2013based model checking of event\u2013driven systems requirements. IEEE Transactions on Software Engineering, 19(1):24\u201340.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"337710_CR3","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1023\/A:1008697817793","volume":"6","author":"R. Bharadwaj","year":"1999","unstructured":"Bharadwaj, R. and Heitmeyer, C.L. 1999. Model checking complete requirements specifications using abstractions. Automated Software Engineering, 6(1):37\u201368.","journal-title":"Automated Software Engineering"},{"key":"337710_CR4","series-title":"Springer Computer Science","volume-title":"Design, specification and verification of interactive systems `96","year":"1996","unstructured":"Bodart, F. and Vanderdonckt, J. (eds.) 1996. Design, specification and verification of interactive systems `96, Springer Computer Science. Springer\u2013Verlag\/Wien."},{"issue":"1","key":"337710_CR5","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T. Bolognesi","year":"1987","unstructured":"Bolognesi, T. and Brinksma, E. 1987. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14(1):25\u201359.","journal-title":"Computer Networks and ISDN Systems"},{"key":"337710_CR6","first-page":"347","volume-title":"Validating properties of component\u2013based graphical user interfaces","author":"P. Bumbulis","year":"1996","unstructured":"Bumbulis, P., Alencar, P.S.C., Cowan, D.D., and Lucena, C.J.P. 1996. Validating properties of component\u2013based graphical user interfaces. In Bodart and Vanderdonckt, editors, 1996. Springer\u2013Verlag\/Wien, pp. 347\u2013365."},{"key":"337710_CR7","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., and McMillan, K.L. 1990. Symbolic model checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic In Computer Science, IEEE Computer Society Press, pp. 428\u2013439.","DOI":"10.1109\/LICS.1990.113767"},{"key":"337710_CR8","unstructured":"Campos, J.C. 1999. Automated deduction and usability reasoning. DPhil thesis, Department of Computer Science, University of York."},{"key":"337710_CR9","first-page":"109","volume-title":"Formally verifying interactive systems: A review","author":"J.C. Campos","year":"1997","unstructured":"Campos, J.C. and Harrison, M.D. 1997. Formally verifying interactive systems: A review. In Harrison and Torres, editors, 1997. Springer\u2013Verlag\/Wien, pp. 109\u2013124."},{"key":"337710_CR10","series-title":"Springer Computer Science","first-page":"155","volume-title":"Design, Specification and Verification of Interactive Systems '98","author":"J.C. Campos","year":"1998","unstructured":"Campos, J.C. and Harrison, M.D. 1998. The role of verification in interactive systems design. In P. Markopoulos and P. Johnson, editors, Design, Specification and Verification of Interactive Systems '98, Springer Computer Science, Springer\u2013Verlag\/Wien, pp. 155\u2013170."},{"key":"337710_CR11","series-title":"Springer Computer Science","first-page":"167","volume-title":"Design, Specification and Verification of Interactive Systems '99","author":"J.C. Campos","year":"1999","unstructured":"Campos, J.C. and Harrison, M.D. 1999. Using automated reasoning in the design of an audio\u2013visual communication system. In D.J. Duke and A. Puerta, editors, Design, Specification and Verification of Interactive Systems '99, Springer Computer Science, Springer\u2013Verlag\/Wien, pp. 167\u2013188."},{"issue":"7","key":"337710_CR12","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., and Reese, J.D. 1998. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498\u2013520.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"337710_CR13","unstructured":"Cheaney, E. 1991. ASRS Introduces.... ASRS Directline (1). http:\/\/asrs.arc.nasa.gov\/directline.htm."},{"issue":"4es","key":"337710_CR14","doi-asserted-by":"crossref","first-page":"116\u2013es","DOI":"10.1145\/242224.242374","volume":"28","author":"E. Clarke","year":"1996","unstructured":"Clarke, E. and Wing, J.M. 1996. Tools and partial analysis. ACM Computing Surveys, 28(4es):116\u2013es.","journal-title":"ACM Computing Surveys"},{"issue":"2","key":"337710_CR15","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., and Sistla, A.P. 1986. Automatic verification of finite\u2013state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"337710_CR16","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., and Peled, D. 1999. Model Checking, MIT Press, Cambridge, Massachusetts, U.S.A."},{"key":"337710_CR17","doi-asserted-by":"crossref","unstructured":"de Roever, W.\u2013P. 1998. The need for compositional proof systems: A survey. In W.\u2013P. de Roever, H. Langmaack, and A. Pnueli, editors, Compositionality: The Significant Difference, Springer, pp. 1\u201322. Vol. 1536 of Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-49213-5_1"},{"key":"337710_CR18","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/PL00003934","volume":"12","author":"G. Doherty","year":"2000","unstructured":"Doherty, G., Campos, J.C., and Harrison, M.D. 2000. Representational reasoning and verification. Formal Aspects of Computing, 12:260\u2013277.","journal-title":"Formal Aspects of Computing"},{"key":"337710_CR19","doi-asserted-by":"crossref","unstructured":"Duke, D., Barnard, P., May, J., and Duce, D. 1995. Systematic development of the human interface. In Asia Pacific Software Engineering Conference. IEEE Computer Society Press, pp. 313\u2013321.","DOI":"10.1109\/APSEC.1995.496980"},{"issue":"3","key":"337710_CR20","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1111\/1467-8659.1230025","volume":"12","author":"D.J. Duke","year":"1993","unstructured":"Duke, D.J. and Harrison, M.D. 1993. Abstract interaction objects. Computer Graphics Forum, 12(3):25\u201336.","journal-title":"Computer Graphics Forum"},{"key":"337710_CR21","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Carr, V., and Hines, L. 1997. Model checking graphical user interfaces using abstractions. In M. Jazayeri and H. Schauer, editors, Software Engineering\u2014ESEC\/FSE '97, Springer, pp. 244\u2013261. Vol. 1301 of Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-63531-9_18"},{"key":"337710_CR22","unstructured":"Faconti, G. and Patern\u00f2, F. 1990. An approach to the formal specification of the components of an interaction. In C. Vandoni and D. Duce, editors, Eurographics '90. North\u2013Holland, pp. 481\u2013494."},{"issue":"3","key":"337710_CR23","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1093\/logcom\/1.3.357","volume":"1","author":"J. Fiadeiro","year":"1991","unstructured":"Fiadeiro, J. and Maibaum, T. 1991. Temporal reasoning over deontic specifications. Journal of Logic and Computation 1(3):357\u2013395.","journal-title":"Journal of Logic and Computation"},{"key":"337710_CR24","first-page":"29","volume-title":"DMVIS: Design, modelling and validation of interactive systems","author":"B. Fields","year":"1997","unstructured":"Fields, B., Merriam, N., and Dearden, A. 1997. DMVIS: Design, modelling and validation of interactive systems. In Harrison and Torres, editors, 1997. Springer\u2013Verlag\/Wien, pp. 29\u201344."},{"key":"337710_CR25","volume-title":"Formal Aspects of the Human Computer Interface, electronic, Workshops in Computing","author":"M. Harrison","year":"1996","unstructured":"Harrison, M., Fields, R., and Wright, P.C. 1996. The user context and formal specification in interactive system design (invited paper). In C.R. Roast and J.I. Siddiqi, editors, Formal Aspects of the Human Computer Interface, electronic, Workshops in Computing. London: Springer\u2013Verlag."},{"key":"337710_CR26","series-title":"Springer Computer Science, Eurographics","volume-title":"Design, specification and verification of interactive systems `97","year":"1997","unstructured":"Harrison, M.D. and Torres, J.C. (eds.) 1997. Design, specification and verification of interactive systems `97, Springer Computer Science, Eurographics, Springer\u2013Verlag\/Wien."},{"key":"337710_CR27","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C., Kirby, J., and Labaw, B. 1998. Applying the SRC requirements method to a weapons control panel: An experience report. In Proceedings of the Second Workshop on Formal Methods in Software Practice (FMSP '98), pp. 92\u2013102.","DOI":"10.1145\/298595.298863"},{"issue":"4es","key":"337710_CR28","doi-asserted-by":"crossref","first-page":"119\u2013es","DOI":"10.1145\/242224.242378","volume":"28","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A. 1996. Some myths about formal verification. ACM Computing Surveys, 28(4es):119\u2013es.","journal-title":"ACM Computing Surveys"},{"key":"337710_CR29","volume-title":"SAS MD\u201380: Flight management system guide","author":"Honeywell Inc.","year":"1988","unstructured":"Honeywell Inc. 1988. SAS MD\u201380: Flight management system guide. Honeywell Inc., Sperry Commercial Flight Systems Group, Air Transport Systems Division, P.O. Box 21111, Phoenix, Arizona 85036, USA. Pub. No. C28\u20133642\u201322\u201301."},{"key":"337710_CR30","unstructured":"Leveson, N.G. and Palmer, E. 1997. Designing automation to reduce operator errors. In Proceedings of the IEEE Systems, Man, and Cybernetics Conference."},{"key":"337710_CR31","unstructured":"Ma\u00f1as, J.A. et al. 1992. Lite user manual. LOTOSPHERE consortium. Ref. Lo\/WP2\/N0034\/V08."},{"key":"337710_CR32","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L. 1993. Symbolic Model Checking, Kluwer Academic Publishers, USA."},{"key":"337710_CR33","doi-asserted-by":"crossref","unstructured":"Monk, A.F. and Curry, M.B. 1994. Discount dialogue modelling with action simulator. In G. Cockton, S.W. Draper, and G.R.S. Weir, editors, People and Computer IX\u2014Proceedings of HCI'94. Cambridge University Press, pp. 327\u2013338.","DOI":"10.1017\/CBO9780511600821.025"},{"issue":"7","key":"337710_CR34","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1016\/0169-7552(93)90047-8","volume":"25","author":"R.D. Nicola","year":"1993","unstructured":"Nicola, R.D., Fantechi, A., Gnesi, S., and Ristori, G. 1993. An action\u2013based framework for verifying logical and behavioural properties of concurrent systems. Computer Networks and ISDN Systems, 25(7):761\u2013778.","journal-title":"Computer Networks and ISDN Systems"},{"key":"337710_CR35","doi-asserted-by":"crossref","unstructured":"Palanque, P., Patern\u00f2, F., Bastide, R., and Mezzanote, M., 1996. Towards an integrated proposal for interactive systems design based on TLIM and ICO. In Bodart and Vanderdonckt, 1996, pp. 162\u2013187.","DOI":"10.1007\/978-3-7091-7491-3_9"},{"key":"337710_CR36","unstructured":"Palmer, E. 1995. Oops, it didn't arm\u2014A case study of two automation surprises. In R.S. Jensen and L.A. Rakovan, editors, Proceedings of the Eighth International Symposium on Aviation Psychology. Columbus, Ohio, pp. 227\u2013232."},{"key":"337710_CR37","unstructured":"Patern\u00f2, F. and Mezzanotte, M. 1995. Formal analysis of user and system interactions in the CERD case study. Technical Report SM\/WP48, Amodeus Project."},{"key":"337710_CR38","unstructured":"Patern\u00f2, F.D. 1995. A method for formal specification and verification of interactive systems. Ph.D. thesis, Department of Computer Science, University of York."},{"key":"337710_CR39","unstructured":"Rushby, J. 1999. Using model checking to help discover mode confusions and other automation surprises. In (Pre\u2013) Proceedings of the Workshop on Human Error, Safety, and System Development (HESSD) 1999. Li\u00e8ge, Belgium."},{"key":"337710_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"569","DOI":"10.1007\/3-540-54415-1_65","volume-title":"Theoretical Aspects of Computer Software","author":"M. Ryan","year":"1991","unstructured":"Ryan, M., Fiadeiro, J., and Maibaum, T. 1991. Sharing actions and attributes in modal action logic. In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Software, Springer\u2013Verlag, pp. 569\u2013593. Vol. 526 of Lecture Notes in Computer Science, Berlin Heidelberg, New York."},{"key":"337710_CR41","unstructured":"Sreemani, T. and Atlee, J.M. 1996. Feasibility of model checking software requirements: A case study. In Proceedings of the 11th Annual Conference on Computer Assurance (COMPASS '96), pp. 77\u201388."},{"key":"337710_CR42","unstructured":"Stallman, R. 1998. GNU Emacs Manual. 13th edition. Free Software Foundation."},{"key":"337710_CR43","unstructured":"Wall, L., Christiansen, T., and Schwartz, R.L. 1996. Programming Perl, 2nd edition. O'Reilly & Associates, Inc."},{"key":"337710_CR44","unstructured":"Woods, D.D., Johannesen, L.J., Cook, R.I., and Sarter, N.B. 1994. Behind human error: Cognitive systems, computers, and hindsight. State\u2013of\u2013the\u2013Art Report SOAR 94\u201301, CSERIAC."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011265604021.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011265604021\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011265604021.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:32:34Z","timestamp":1748071954000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011265604021"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,8]]},"references-count":44,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2001,8]]}},"alternative-id":["337710"],"URL":"https:\/\/doi.org\/10.1023\/a:1011265604021","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,8]]}}}