{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:08:13Z","timestamp":1725458893075},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590088"},{"type":"electronic","value":"9783540491736"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0035813","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:36:05Z","timestamp":1138203365000},"page":"159-173","source":"Crossref","is-referenced-by-count":7,"title":["From formal models to formal methods"],"prefix":"10.1007","author":[{"given":"D. J.","family":"Duke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. D.","family":"Harrison","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"14_CR1","unstructured":"G. Abowd. Formal aspects of human-computer interaction. D.Phil Thesis, Oxford University Computing Laboratory: Programming Research Group, 1991. Available as Technical Monograph PRG-97."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"S. Bly, S. Harrison, and S. Irwin. Media spaces: Bringing people together in a video, audio and computing environment. Communications of the ACM, 36(1), January 1993.","DOI":"10.1145\/151233.151235"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"P. Dourish and S. Bly. Portholes: Supporting awareness in distributed work groups. In Proc. ACM Conference on Human Factors in Computer Systems: CHI '92. Addison-Wesley. 1992.","DOI":"10.1145\/142750.142982"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"D.J. Duke, G. Faconti, M.D. Harrison, and F. Paterno'. Unifying views of interactors. In Proc International Workshop on Advanced Visual Interfaces, 1994. To appear.","DOI":"10.1145\/192309.192341"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"D.J. Duke and M.D. Harrison. Abstract interaction objects. Computer Graphics Forum, 12(3), 1993. Conference Issue: Proc. Eurographics'93.","DOI":"10.1111\/1467-8659.1230025"},{"key":"14_CR6","unstructured":"D.J. Duke and M.D. Harrison. Mapping user requirements to implementations. To appear in Software Engineering Journal. Based on Amodeus-2 document sysmod\/sm_wpl6, 1993."},{"key":"14_CR7","unstructured":"D.J. Duke and M.D. Harrison. Connections: From A(V) to Z. Technical Report SM\/WP29, ESPRIT BRA 7040 Amodeus-2, January 1994. File: sysmod\/sm_wp29.ps."},{"key":"14_CR8","unstructured":"D.J. Duke and M.D. Harrison. FSM analysis of access control. Technical Report SM\/WP42, ESPRIT BRA 7040 Amodeus-2, October 1994."},{"key":"14_CR9","unstructured":"D.J. Duke and M.D. Harrison. A preliminary FSM analysis of the CERD. Technical Report SM\/IR8, ESPRIT BRA 7040 Amodeus-2, May 1994."},{"key":"14_CR10","unstructured":"B. Gaver, T. Moran, A. MacLean, L. Lovstrand, P. Dourish, K. Carter, and B. Buxton. Realising a video environment: Europarc's RAVE system. In Proc. ACM Conference on Human Factors in Computer Systems: CHI '92. Addison-Wesley, 1992."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"A. Hall. Seven myths of formal methods. Software, pages 11\u201319, September 1990.","DOI":"10.1109\/52.57887"},{"key":"14_CR12","unstructured":"M.D. Harrison. A model for the option space of interactive systems. In Engineering for Human-Computer Interaction: Proc IFIP WG2.7 Conf. Elsevier, 1992."},{"key":"14_CR13","unstructured":"M.D. Harrison and A. Dix. A state model of direct manipulation. In M.D. Harrison and H.W. Thimbleby, editors, Formal Methods in Human Computer Interaction, pages 129\u2013151. Cambridge University Press, 1990."},{"key":"14_CR14","unstructured":"M.D. Harrison, C.R. Roast, and P.C. Wright. Complementary methods for the iterative design of interactive systems. In G. Salvendy and M. Smith, editors, Designing and Using Human-Computer Interfaces and Knowledge Based Systems. Elsevier Scientific, 1989."},{"key":"14_CR15","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1016\/0020-7373(92)90059-T","volume":"37","author":"C.W. Johnson","year":"1992","unstructured":"C.W. Johnson and M.D. Harrison. Using temporal logic to support the specification and prototyping of interactive control systems. Int. J. Man-Machine Studies, 37:357\u2013385, 1992.","journal-title":"Int. J. Man-Machine Studies"},{"key":"14_CR16","unstructured":"C.B. Jones. Systematic Software Development Using VDM. Prentice Hall International, second edition, 1990."},{"key":"14_CR17","unstructured":"L.S. Marshall. Formally describing interactive systems. In C.B. Jones and R. Shaw, editors, Case Studies in Systematic Software Development, pages 293\u2013336. Prentice Hall, 1990."},{"key":"14_CR18","unstructured":"F. Paterno and G. Faconti. On the use of LOTOS to describe graphical interaction. In A. Monk, D. Diaper, and M. Harrison, editors, People and Computers VII: Proc. of the HCI'92 Conference, Conference Series, pages 155\u2013173. British Computer Society, 1992."},{"key":"14_CR19","unstructured":"B. Sufrin and J. He. Specification, refinement, and analysis of interactive processes. In M.D. Harrison and H.W. Thimbleby, editors, Formal Methods in Human Computer Interaction, pages 153\u2013200. Cambridge University Press, 1990."},{"key":"14_CR20","unstructured":"J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, second edition, 1992."}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Human-Computer Interaction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0035813","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T14:42:18Z","timestamp":1555425738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0035813"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590088","9783540491736"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0035813","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}