{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T05:08:46Z","timestamp":1737176926606,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540428077"},{"type":"electronic","value":"9783540455226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45522-1_9","type":"book-chapter","created":{"date-parts":[[2007,6,18]],"date-time":"2007-06-18T10:22:20Z","timestamp":1182162140000},"page":"144-163","source":"Crossref","is-referenced-by-count":8,"title":["Reasoning about Interactive Systems with Stochastic Models"],"prefix":"10.1007","author":[{"given":"G.","family":"Doherty","sequence":"first","affiliation":[]},{"given":"M.","family":"Massink","sequence":"additional","affiliation":[]},{"given":"G.","family":"Faconti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,10,29]]},"reference":[{"key":"9_CR1","unstructured":"H. Alexander. Structuring dialogues using CSP. In M. D. Harrison and H. W. Thimbleby, editors, Formal methods in Human Computer Interaction, pages 273\u2013295. Cambridge University Press, 1990."},{"key":"9_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming: Proceedings of the18th ICALP","author":"R. Alur","year":"1991","unstructured":"R. Alur, C. Courcoubetis, and D.L. Dill. Model-checking for probabilistic realtimesystems. In Automata, Languages and Programming: Proceedings of the18th ICALP, volume 510 of Lecture Notes in Computer Science, pages 115\u2013136.Springer-Verlag, 1991."},{"key":"9_CR3","unstructured":"Fran\u00e7ois B\u00e9rard. Vision par ordinateur pour l\u2019interaction fortement coupl\u00e9e. PhD thesis, L\u2019Universit\u00e9 Joseph Fourier Grenoble I, 1999."},{"key":"9_CR4","unstructured":"H. Bowman, J. W. Bryans, and J. Derrick. Analysis of a multimedia stream usingstochastic process algebra. InC. Priami, editor, Proceedings of 6th InternationalWorkshop on Process Algebras and Performance Modelling, Nice, France, pages51\u201369, September 1998."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"H. Bowman, G. P. Faconti, and M. Massink. Specification and verification of mediaconstraints using UPPAAL. In P. Markopoulos and P. Johnson, editors, Proceedingsof the 5th Eurographics Workshop on Design, Specification, and Verification ofInteractive Systems, pages 261\u2013277. Springer Wien, 1998.","DOI":"10.1007\/978-3-7091-3693-5_17"},{"key":"9_CR6","unstructured":"J. Bryans, H. Bowman, and J. Derrick. A model checking algorithm for stochasticsystems. Technical Report 4-00, University of Kent at Canterbury, January 2000."},{"key":"9_CR7","unstructured":"P. Cairns, M. Jones, and H. Thimbleby. Reusable usability analysis with markovmodels. ACM Transactions on Human-Computer Interaction, (in press), 2001."},{"key":"9_CR8","unstructured":"S. Card, T. Moran, and A. Newell. The psychology of human computer interaction.Lawrence Erlbaum Associates, 1983."},{"key":"9_CR9","unstructured":"P. R. D\u2019Argenio, J-P. Katoen, and E. Brinksma. A stochastic automaton model andits algebraicapproac h. In Proceedings of 5th International Workshop on ProcessAlgebra and Performance Modelling, pages 1\u201317, 1997. CTIT Technical Report97-09."},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"A.M. Dearden and M.D. Harrison. Using executable interactor specifications to explore the impact of operator interaction error. InP. Daniel, editor, SAFECOMP97: Proceedings of the 16th International Conference Computer Safety, Reliabilityand Security, pages 138\u2013147. Springer, 1997.","DOI":"10.1007\/978-1-4471-0997-6_11"},{"key":"9_CR11","unstructured":"G. Doherty and M. Massink. Stochastic modelling of interactive systems withUML. TUPIS Workshop, UML 2000."},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"G. Doherty, M. Massink, and G. Faconti. Using hybrid automata to support humanfactors analysis in a critical system. Formal Methods in System Design, 19(2),September 2001.","DOI":"10.1023\/A:1011232016683"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"M. Du and D. England. Temporal patterns for complex interaction design. In Johnson [25].","DOI":"10.1007\/3-540-45522-1_7"},{"key":"9_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/3-540-58021-2_20","volume-title":"Proceedings of the SeventhInternational Conference on Modelling Techniques and Tools for Computer PerformanceEvaluation","author":"S. Gilmore","year":"1994","unstructured":"S. Gilmore and J. Hillston. The PEPA workbench: A tool to support a processalgebra-based approach to performance modelling. In Proceedings of the SeventhInternational Conference on Modelling Techniques and Tools for Computer PerformanceEvaluation, volume 794 of Lecture Notes in Computer Science, pages353\u2013368. Springer-Verlag, 1994."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"S. Gnesi, D. Latella, and M. Massink. A stochastic extension of a behaviouralsubset of UML statechart diagrams. In L. Palagi and R. Bilof, editors, Fifth IEEEInternational High-Assurance Systems Engineering Symposium, pages 55\u201364. IEEE Computer Society Press, 2000.","DOI":"10.1109\/HASE.2000.895442"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"M.D. Harrison, A.E. Blandford, and P.J. Barnard. The requirements engineeringof user freedom. InF. Patern\u00f3, editor, Proceedings of Eurographics Workshop on Design Specification and Verification of Interactive Systems, Italy, pages 181\u2013194.Springer-Verlag, 1995.","DOI":"10.1007\/978-3-642-87115-3_16"},{"key":"9_CR17","unstructured":"F. Hartleb. Stochastic graph models for performance evaluation of parallel programsand the evaluation tool PEPP. In Proceedings of the QMIPS Workshop onFormalisms, Principles and State-of-the-art, Erlangen\/Pommersfelden, Germany,number 14 in Arbeitsbericht Band 26, pages 207\u2013224, March 1993."},{"key":"9_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"Proceedings of TACAS 2000","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.P. Katoen, J. Meyer-Kayser, and M. Siegle. Tools and algorithmsfor the construction and analysis of systems. In Proceedings of TACAS 2000,volume 1785 of LNCS, pages 347\u2013362. Springer-Verlag, 2000."},{"key":"9_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1007\/3-540-48683-6_42","volume-title":"Proceedings of CompterAided Verification (CAV) 99","author":"H. Hermanns","year":"1999","unstructured":"H. Hermanns, V. Mertsiotakis, and M. Siegle. TIPPtool: Compositional speci.-cation and analysis of markovian performance models. In Proceedings of CompterAided Verification (CAV) 99, volume 1633 of Lecture Notes in Computer Science,pages 487\u2013490. Springer-Verlag, 1999."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"J. Hillston. A Compositional Approach to Performance Modelling. DistinguishedDissertations in Computer Science. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511569951"},{"key":"9_CR21","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International,1985."},{"issue":"1","key":"9_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/imms.1993.1051","volume":"39","author":"E. Hollnagel","year":"1993","unstructured":"E. Hollnagel. The phenotype of erroneous actions. International Journal of Man-Machine Studies, 39(1):1\u201332, July 1993.","journal-title":"International Journal of Man-Machine Studies"},{"issue":"2","key":"9_CR23","first-page":"309","volume":"6","author":"R. Jagacinski","year":"1980","unstructured":"R. Jagacinski, R.D. Repperger, M. Moran, S. Ward, and B. Glass. Fitts\u2019 law and themicrostructure of rapid discrete movements. Journal of Experimental Psychology:Human Perception and Performance, 6(2):309\u2013320, 1980.","journal-title":"Journal of Experimental Psychology:Human Perception and Performance"},{"key":"9_CR24","volume-title":"The art of computer systems performance analysis: techniques for experimentaldesign, measurement, simulation, and modeling","author":"R. Jain","year":"1991","unstructured":"R. Jain. The art of computer systems performance analysis: techniques for experimentaldesign, measurement, simulation, and modeling. Wiley, New York, 1991."},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"C. Johnson, editor. Proceedings of Design Specification and Verification of InteractiveSystems, Glasgow. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45522-1"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1080\/00222895.1976.10735061","volume":"8","author":"G. Langolf","year":"1976","unstructured":"G. Langolf, D. Chaffin, and J. Foulke. An investigation of Fitts\u2019 law. Journal of Motor Behaviour, 8:113\u2013128, 1976.","journal-title":"Journal of Motor Behaviour"},{"key":"9_CR27","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1207\/s15327051hci0701_3","volume":"7","author":"I. S. MacKenzie","year":"1992","unstructured":"I. Scott MacKenzie. Fitts\u2019 law as a research and design tool in human-computerinteraction. Human Computer Interaction, 7:91\u2013139, 1992.","journal-title":"Human Computer Interaction"},{"key":"9_CR28","unstructured":"D. Navarre, P. Palanque, F. Paterno, C. Santoro, and R. Bastide. Tool suite forintegrating task and system models through scenarios. In Johnson [25]."},{"key":"9_CR29","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/S0953-5438(97)00013-1","volume":"9","author":"P. Palanque","year":"1997","unstructured":"P. Palanque and R. Bastide. Synergisticmo delling of tasks, users and systems usingformal specification techniques. Interacting with Computers, 9:129\u2013153, 1997.","journal-title":"Interacting with Computers"},{"key":"9_CR30","unstructured":"J. Pearl. Probabilistic Reasoning in Intelligent Systems: Networks of PlausibleInference. San Mateo, CA: Morgan Kaufmann, 1988."},{"key":"9_CR31","unstructured":"G. Salvendy, editor. Handbook of Human Factors and Ergonomics. Wiley-Interscience, 2nd edition, 1997."},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"R. Sch\u00e4fer and Thomas Weyrath. Assessing temporally variable user properties with dynamicba yesian networks. InA. Jameson, C. Paris, and C. Tasso, editors,User Modelling: Proceedings of the Sixth Internation Conference. Springer Wien New York, 1997.","DOI":"10.1007\/978-3-7091-2670-7_38"},{"key":"9_CR33","unstructured":"A.D. Swain and H.E. Guttmann. Handbook of human reliability analysis withemphasis on nuclear power plant applications-final report. Technical Report NRC FIN A 1188 NUREG\/CR-1278 SAND80-0200, Prepared for Division of FacilityOperations; Office of Nuclear Regulatory Research; US Nuclear RegulatoryCommission; Washington, D.C. 20555, August 1983."},{"key":"9_CR34","unstructured":"M.Q.V. Turnell, A. Scaico, M.R.F. de Sousa, and A. Perkusich. Industrial user interfaceevaluation based on coloured petri nets modelling and analysis. In Johnson[25]."},{"issue":"4","key":"9_CR35","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1145\/198425.198426","volume":"1","author":"C. Ware","year":"1994","unstructured":"C. Ware and R. Balakrishnan. Reaching for objects in VR displays: Lag andframe rate. ACM Transactions on Human Computer Interaction, 1(4):331\u2013356,December 1994.","journal-title":"ACM Transactions on Human Computer Interaction"},{"key":"9_CR36","unstructured":"C.D. Wickens. Engineering Psychology and Human Performance. Charles E. Merrill Publishing Company, 1984."}],"container-title":["Lecture Notes in Computer Science","Interactive Systems: Design, Specification, and Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45522-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T08:36:46Z","timestamp":1737103006000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45522-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540428077","9783540455226"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-45522-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}