{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:52:21Z","timestamp":1756000341911},"publisher-location":"Vienna","reference-count":26,"publisher":"Springer Vienna","isbn-type":[{"type":"print","value":"9783211830550"},{"type":"electronic","value":"9783709168783"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/978-3-7091-6878-3_8","type":"book-chapter","created":{"date-parts":[[2011,9,15]],"date-time":"2011-09-15T07:43:51Z","timestamp":1316072631000},"page":"109-124","source":"Crossref","is-referenced-by-count":24,"title":["Formally Verifying Interactive Systems: A Review"],"prefix":"10.1007","author":[{"given":"Jos\u00e9 C.","family":"Campos","sequence":"first","affiliation":[]},{"given":"Michael D.","family":"Harrison","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","first-page":"219","volume-title":"Proceedings of the First Symposium of Designing Interactive Systems - DIS\u201995","author":"GD Abowd","year":"1995","unstructured":"Gregory D. Abowd, Hung-Ming Wang, and Andrew F. Monk. A formal technique for automated dialogue development. In Proceedings of the First Symposium of Designing Interactive Systems - DIS\u201995, pages 219 \u2013 226. ACM Press, August 1995."},{"volume-title":"Design, Specification and Verification of Interactive Systems \u201996, Springer Computer Science","year":"1996","key":"8_CR2","unstructured":"F. Bodart and J. Vanderdonckt, editors. Design, Specification and Verification of Interactive Systems \u201996, Springer Computer Science. Springer-Verlag\/Vien, June 1996."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Peter Bumbulis, P. S. C. Alencar, D. D. Cowan, and C. J. P. Lucena. Validating properties of component-based graphical user interfaces. In Bodart and Vanderdonckt [2], pages 347\u2013365.","DOI":"10.1007\/978-3-7091-7491-3_18"},{"key":"8_CR4","volume-title":"States and Beyond","author":"JR Burch","year":"1990","unstructured":"J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. In L\/CS, 1990."},{"issue":"(2)","key":"8_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"E. M. Clarke, 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, 8 (2): 244 \u2013 263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Bruno d\u2019Ausbourg, Guy Durrieu, and Pierre Roche. Deriving a formal model of an interactive system from its uil description in order to verify and to test its behaviour. In Bodart and Vanderdonckt [2], pages 105\u2013122.","DOI":"10.1007\/978-3-7091-7491-3_6"},{"issue":"(6)","key":"8_CR7","first-page":"324","volume":"11","author":"A Dix","year":"1996","unstructured":"Alan Dix and Gregory Abowd. Modelling status and event behaviour of interactive systems. Software Engeneering Journal, 11 (6): 324 \u2013 346, November 1996.","journal-title":"Software Engeneering Journal"},{"key":"8_CR8","volume-title":"Prentice Hall","author":"A Dix","year":"1993","unstructured":"Alan Dix, Janet Finlay, Gregory Abowd, and Russell Beale. Human-Computer Interaction. Prentice Hall, 1993."},{"key":"8_CR9","volume-title":"Technical Report System Modelling\/D9","author":"D Duke","year":"1995","unstructured":"David Duke, Michael Harrison, J\u00f6elle Coutaz, Laurence Nigay, Daniel Salber, Giorgio Faconti, Menica Mezzanotte, Fabio Paterno, and David Duce. The Amodeus system reference model. Technical Report System Modelling\/D9, Amodeus Project, June 1995."},{"issue":"(3)","key":"8_CR10","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1111\/1467-8659.1230025","volume":"12","author":"DJ Duke","year":"1993","unstructured":"David J. Duke and Michael D. Harrison. Abstract interaction objects. Computer Graphics Forum, 12 (3): 25 \u2013 36, 1993.","journal-title":"Computer Graphics Forum"},{"key":"8_CR11","first-page":"313","volume-title":"Asia Pacific Software Engeneering Conference","author":"DJ Duke","year":"1995","unstructured":"D.J. Duke, P.J. Barnard, J. May, and D.A. Duce. Systematic development of the human interface. In Asia Pacific Software Engeneering Conference, pages 313 \u2013 321. IEEE Computer Society Press, December 1995."},{"key":"8_CR12","volume-title":"Computer Aided Verification, Proceedings of the Fourth International Workshop, CAV\u201992, volume 663 of Lecture Notes in Computer Science. Springer-Verlag","author":"U Engberg","year":"1992","unstructured":"Urban Engberg, Peter Gr\u00f8nning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In Computer Aided Verification, Proceedings of the Fourth International Workshop, CAV\u201992, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, 1992."},{"key":"8_CR13","volume-title":"A method for user interface development in safety-critical applications","author":"B Fields","year":"1996","unstructured":"Bob Fields, Peter Wright, and Michael Harrison. A method for user interface development in safety-critical applications. Human-Computer Interaction Group, University of York (unpublished ), 1996."},{"issue":"(3)","key":"8_CR14","first-page":"243","volume":"5","author":"Mark Green","year":"1986","unstructured":"Mark Green. A survey of three dialogue models. ACM Transactions on Graphics, 5 (3): 243 \u2013 275, July 1986.","journal-title":"ACM Transactions on Graphics"},{"key":"8_CR15","volume-title":"Springer-Verlag","author":"JV Guttag","year":"1993","unstructured":"John V. Guttag, James J. Horning, et al. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993."},{"issue":"(3)","key":"8_CR16","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"Leslie Lamport","year":"1994","unstructured":"Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16 (3): 872 \u2013 923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR17","volume-title":"Safeware: System Safety and Computers","author":"Nancy Leveson","year":"1995","unstructured":"Nancy Leveson. Safeware: System Safety and Computers. Addison-Wesley Publishing Company, Inc., 1995."},{"key":"8_CR18","unstructured":"Jos\u00e9 A. Ma\u00f1as et al. Lite User Manual. LOTOSPHERE consortium, March 1992. Ref. Lo\/WP2\/N0034\/V08."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"8_CR20","volume-title":"G. Cockton, S. W. Draper, and G. R. S. Weir, editors, People and Computer IX - Proceedings ofHCI\u201994, pages 327\u2013338. Cambridge University Press","author":"AF Monk","year":"1994","unstructured":"Andrew F. Monk and Martin B. Curry. Discount dialogue modelling with Action Simulator. In G. Cockton, S. W. Draper, and G. R. S. Weir, editors, People and Computer IX - Proceedings ofHCI\u201994, pages 327\u2013338. Cambridge University Press, 1994."},{"issue":"(7)","key":"8_CR21","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1016\/0169-7552(93)90047-8","volume":"25","author":"R Nicola De","year":"1993","unstructured":"R. De Nicola, A. Fantechi, S. Gnesi, and G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Networks and ISDN Systems, 25 (7): 761 \u2013 778, February 1993.","journal-title":"Computer Networks and ISDN Systems"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Philippe Palanque, Fabio Paterno, Remi Bastide, and Menica Mezzanote. Towards an integrated proposal for interactive systems design based on TLIM and ICO. In Bodart and Vanderdonckt [2], pages 162\u2013187.","DOI":"10.1007\/978-3-7091-7491-3_9"},{"key":"8_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-87115-3","volume-title":"A Method for Formal Specification and Verification of Interactive Systems. PhD thesis","author":"Fabio Paterno","year":"1995","unstructured":"Fabio Paterno. A Method for Formal Specification and Verification of Interactive Systems. PhD thesis, Department of Computer Science, University of York, 1995."},{"key":"8_CR24","first-page":"84","volume-title":"Computer-Aided Verification, CAV\u201995, volume 939 of Lecture Notes in Computer Science","author":"S Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Computer-Aided Verification, CAV\u201995, volume 939 of Lecture Notes in Computer Science, pages 84 \u2013 97. Springer Verlag, July 1995."},{"key":"8_CR25","unstructured":"Harold Thimbleby. User Interface Design. Frontier Series. ACM Press, 1990."},{"key":"8_CR26","doi-asserted-by":"crossref","DOI":"10.21236\/ADA286065","volume-title":"A tabular interface for automated verification of event-based dialogs","author":"H-M Wang","year":"1994","unstructured":"Hung-Ming Wang and Gregory D. Abowd. A tabular interface for automated verification of event-based dialogs. Technical Report CMU-CS-94-189, Department of Computer Science, Carnegie Mellon University, July 1994."}],"container-title":["Eurographics","Design, Specification and Verification of Interactive Systems \u201997"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-7091-6878-3_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,6]],"date-time":"2021-05-06T15:34:47Z","timestamp":1620315287000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-7091-6878-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783211830550","9783709168783"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-7091-6878-3_8","relation":{},"ISSN":["0946-2767"],"issn-type":[{"type":"print","value":"0946-2767"}],"subject":[],"published":{"date-parts":[[1997]]}}}