{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:45:38Z","timestamp":1743039938060,"version":"3.40.3"},"publisher-location":"Cham","reference-count":84,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030549930"},{"type":"electronic","value":"9783030549947"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-54994-7_33","type":"book-chapter","created":{"date-parts":[[2020,8,12]],"date-time":"2020-08-12T20:03:45Z","timestamp":1597262625000},"page":"443-464","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Survey of Papers from Formal Methods for Interactive Systems (FMIS) Workshops"],"prefix":"10.1007","author":[{"given":"Pascal","family":"B\u00e9ger","sequence":"first","affiliation":[]},{"given":"Sebastien","family":"Leriche","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Prun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,8,13]]},"reference":[{"key":"33_CR1","unstructured":"Ed 143 - minimum operational performance standards for traffic alert and collision avoidance system ii (tcas ii), April 2013"},{"key":"33_CR2","unstructured":"Bargh, J.A.: The four horsemen of automaticity: awareness, efficiency, intention, and control in social cognition, vol. 2, January 1994"},{"key":"33_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"33_CR4","unstructured":"Ament, M., Cox, A., Blandford, A., Brumby, D.: Working memory load affects device-specific but not task-specific error rate. In: CogSci 2010: Proceedings of the Annual Conference of the Cognitive Science Society, pp. 91\u201396 (2010)"},{"key":"33_CR5","doi-asserted-by":"publisher","unstructured":"Anderson, H., Ciobanu, G.: Markov abstractions for probabilistic pi-calculus. Electr. Commun. EASST 22 (2009). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.22.317","DOI":"10.14279\/tuj.eceasst.22.317"},{"key":"33_CR6","unstructured":"Arapinis, M., et al.: Towards the verification of pervasive systems. Electr. Commun. EASST 22 (2009)"},{"issue":"2","key":"33_CR7","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/j.tcs.2004.07.036","volume":"335","author":"J Baeten","year":"2005","unstructured":"Baeten, J.: A brief history of process algebra. Theoretical Computer Science 335(2), 131\u2013146 (2005). Process Algebra","journal-title":"Theoretical Computer Science"},{"key":"33_CR8","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Banach, R., Razavi, J., Debicki, O., Mareau, N., Lesecq, S., Foucault, J.: Application of formal methods in the inspex smart systems integration project. In: FMIS 2018, May 2018","DOI":"10.1007\/978-3-030-04771-9_16"},{"key":"33_CR10","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.entcs.2007.01.063","volume":"183","author":"MA Barbosa","year":"2007","unstructured":"Barbosa, M.A., Barbosa, L.S., Campos, J.C.: Towards a coordination model for interactive systems. Electr. Notes Theoret. Comput. Sci. 183, 89\u2013103 (2007). Proceedings of the First International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005). \n                    https:\/\/doi.org\/10.1007\/978-3-540-30569-9_3"},{"key":"33_CR12","unstructured":"Bass, E.J., Feigh, K.M., Gunter, E., Rushby, J.: Formal modeling and analysis for interactive hybrid systems. ECEASST 45 (2011)"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Beaudouin-Lafon, M.: Designing interaction, not interfaces. In: Proceedings of the Working Conference on Advanced Visual Interfaces, AVI 2004, pp. 15\u201322. ACM, New York (2004)","DOI":"10.1145\/989863.989865"},{"key":"33_CR14","unstructured":"Beckert, B., Beuster, G.: Guaranteeing consistency in text-based human-computer-interaction. In: proceedings of the First International Workshop on Formal Methods for Interactive Systems (2007)"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"33_CR16","unstructured":"Bhandal, C., Bouroche, M., Hughes, A.: A process algebraic description of a temporal wireless network protocol. ECEASST 45 (2011)"},{"key":"33_CR17","unstructured":"Bhattacharya, S., Basu, A., Samanta, D., Bhattacherjee, S., Srivatava, A.: Some issues in modeling the performance of soft keyboards with scanning. In: proceedings of the First International Workshop on Formal Methods for Interactive Systems (2007)"},{"issue":"7","key":"33_CR18","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1017\/S0960129514000437","volume":"26","author":"S Boldo","year":"2016","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196\u20131233 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"key":"33_CR19","doi-asserted-by":"publisher","unstructured":"Bonnefon, J.F., Longin, D., Nguyen, M.H.: A logical framework for trust-related emotions. Electr. Commun. EASST 22 (2009). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.22.315.312","DOI":"10.14279\/tuj.eceasst.22.315.312"},{"key":"33_CR20","unstructured":"Bowen, J., Hinze, A.: Supporting mobile application development with model-driven emulation 45 (2011)"},{"key":"33_CR21","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.entcs.2007.01.061","volume":"183","author":"J Bowen","year":"2007","unstructured":"Bowen, J., Reeves, S.: Formal models for informal GUI designs. Electr. Notes Theoret. Comput. Sci. 183, 57\u201372 (2007). Proceedings of the First International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"33_CR22","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2008.03.104","volume":"208","author":"J Bowen","year":"2008","unstructured":"Bowen, J., Reeves, S.: Refinement for user interface designs. Electr. Notes Theoret. Comput. Sci. 208, 5\u201322 (2008). Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"33_CR23","doi-asserted-by":"publisher","unstructured":"Bowen, J., Reeves, S.: Ui-design driven model-based testing. Electr. Commun. EASST 22 (2009). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.22.314","DOI":"10.14279\/tuj.eceasst.22.314"},{"key":"33_CR24","unstructured":"B\u00e9ger, P., Becquet, V., Leriche, S., Prun, D.: Contribution \u00e1 la formalisation des propri\u00e9t\u00e9s graphiques des syst\u00e8mes interactifs pour la validation automatique. In: Afadl 2019. Toulouse, France, June 2019"},{"key":"33_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification: Model-Checking Techniques and Tools","author":"B B\u00e9rard","year":"2010","unstructured":"B\u00e9rard, B., et al.: Systems and Software Verification: Model-Checking Techniques and Tools, 1st edn. Springer Publishing Company Incorporated, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-662-04558-9","edition":"1"},{"key":"33_CR26","doi-asserted-by":"publisher","unstructured":"Calder, M., Gray, P., Unsworth, C.: Tightly coupled verification of pervasive systems. Electr. Commun. EASST 22 (2009). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.22.320","DOI":"10.14279\/tuj.eceasst.22.320"},{"key":"33_CR27","unstructured":"Campos, J., Harrison, M.: Modelling and analysing the interactive behaviour of an infusion pump. ECEASST 45 (2011)"},{"key":"33_CR28","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2007.01.060","volume":"183","author":"D Cansell","year":"2007","unstructured":"Cansell, D., Gibson, J.P., M\u00e9ry, D.: Refinement: a constructive approach to formal software design for a secure e-voting interface. Electr. Notes Theoret. Comput. Sci. 183, 39\u201355 (2007). Proceedings of the First International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"issue":"3","key":"33_CR29","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/j.cognition.2006.01.002","volume":"102","author":"U Cartwright-Finch","year":"2007","unstructured":"Cartwright-Finch, U., Lavie, N.: The role of perceptual load in inattentional blindness. Cognition 102(3), 321\u2013340 (2007)","journal-title":"Cognition"},{"key":"33_CR30","unstructured":"Cerone, A.: Closure and attention activation in human automatic behaviour: a framework for the formal analysis of interactive systems. ECEASST 45 (2011)"},{"key":"33_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-04771-9_17","volume-title":"Software Technologies: Applications and Foundations","author":"A Cerone","year":"2018","unstructured":"Cerone, A.: Towards a cognitive architecture for the formal analysis of human behaviour and learning. In: Mazzara, M., Ober, I., Sala\u00fcn, G. (eds.) STAF 2018. LNCS, vol. 11176, pp. 216\u2013232. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-04771-9_17"},{"key":"33_CR32","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.01.058","volume":"183","author":"A Cerone","year":"2007","unstructured":"Cerone, A., Elbegbayan, N.: Model-checking driven design of interactive systems. Electr. Notes Theoret. Comput. Sci. 183, 3\u201320 (2007). Proceedings of the First International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"33_CR33","doi-asserted-by":"publisher","unstructured":"Cerone, A., Zhao, Y.: Stochastic modelling and analysis of driver behaviour. ECEASST 69 (2013). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.69.965.946","DOI":"10.14279\/tuj.eceasst.69.965.946"},{"key":"33_CR34","volume-title":"The Concurrency Workbench of the New Century","author":"R Cleaveland","year":"2000","unstructured":"Cleaveland, R., Li, T., Sims, S.: The Concurrency Workbench of the New Century. User\u2019s manual SUNY at Stony Brook, Stony Brooke (2000)"},{"key":"33_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10669-9","volume-title":"Discrete, Continuous, and Hybrid Petri Nets","author":"R David","year":"2010","unstructured":"David, R., Alla, H.: Discrete, Continuous, and Hybrid Petri Nets, 2nd edn. Springer Publishing Company Incorporated, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-10669-9","edition":"2"},{"key":"33_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-540-70569-7_5","volume-title":"Interactive Systems. Design, Specification, and Verification","author":"A Dittmar","year":"2008","unstructured":"Dittmar, A., H\u00fcbner, T., Forbrig, P.: HOPS: a prototypical specification tool for interactive systems. In: Graham, T.C.N., Palanque, P. (eds.) DSV-IS 2008. LNCS, vol. 5136, pp. 58\u201371. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-70569-7_5"},{"key":"33_CR37","doi-asserted-by":"publisher","unstructured":"Dittmar, A., Schachtschneider, R.: Lightweight interaction modeling in evolutionary prototyping. ECEASST 69 (2013). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.69.961","DOI":"10.14279\/tuj.eceasst.69.961"},{"key":"33_CR38","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.entcs.2008.03.105","volume":"208","author":"A Dix","year":"2008","unstructured":"Dix, A., Ghazali, M., Ramduny-Ellis, D.: Modelling devices for natural interaction. Electronic Notes in Theoretical Computer Science 208, 23\u201340 (2008). Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"33_CR39","first-page":"849","volume":"18","author":"EJ Raymond","year":"1992","unstructured":"Raymond, E.J., Shapiro, K., Arnell, K.: Temporary suppression of visual processing in an RSVP task: An attentional blink? J. Exp. Psychol. 18, 849\u2013860 (1992). Human perception and performance","journal-title":"J. Exp. Psychol."},{"key":"33_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-030-04771-9_19","volume-title":"Software Technologies: Applications and Foundations","author":"R Geniet","year":"2018","unstructured":"Geniet, R., Singh, N.K.: Refinement based formal development of human-machine interface. In: Mazzara, M., Ober, I., Sala\u00fcn, G. (eds.) STAF 2018. LNCS, vol. 11176, pp. 240\u2013256. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-04771-9_19"},{"key":"33_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-36103-0_34","volume-title":"Formal Methods and Software Engineering","author":"D Goldson","year":"2002","unstructured":"Goldson, D., Reeve, G., Reeves, S.: $${\\mu }$$-chart-based specification and refinement. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 323\u2013334. Springer, Heidelberg (2002). \n                    https:\/\/doi.org\/10.1007\/3-540-36103-0_34"},{"key":"33_CR42","unstructured":"Goranko, V., Galton, A.: Temporal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Winter 2015 Edn. (2015)"},{"key":"33_CR43","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/978-81-322-2268-2_59","volume-title":"Intelligent Computing and Applications","author":"A Gosain","year":"2015","unstructured":"Gosain, A., Sharma, G.: Static analysis: a survey of techniques and tools. In: Mandal, D., Kar, R., Das, S., Panigrahi, B.K. (eds.) Intelligent Computing and Applications. AISC, vol. 343, pp. 581\u2013591. Springer, New Delhi (2015). \n                    https:\/\/doi.org\/10.1007\/978-81-322-2268-2_59"},{"key":"33_CR44","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.entcs.2008.03.106","volume":"208","author":"MD Harrison","year":"2008","unstructured":"Harrison, M.D., Kray, C., Campos, J.C.: Exploring an option space to engineer a ubiquitous computing system. Electr. Notes Theoret. Comput. Sci. 208, 41\u201355 (2008). Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"33_CR45","doi-asserted-by":"publisher","unstructured":"Harrison, M.D., Masci, P., Campos, J.C., Curzon, P.: Automated theorem proving for the systematic analysis of an infusion pump. ECEASST 69 (2013). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.69.962","DOI":"10.14279\/tuj.eceasst.69.962"},{"key":"33_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-030-04771-9_21","volume-title":"Software Technologies: Applications and Foundations","author":"MD Harrison","year":"2018","unstructured":"Harrison, M.D., Masci, P., Campos, J.C.: Formal modelling as a component of user centred design. In: Mazzara, M., Ober, I., Sala\u00fcn, G. (eds.) STAF 2018. LNCS, vol. 11176, pp. 274\u2013289. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-04771-9_21"},{"key":"33_CR47","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951","volume-title":"A Compositional Approach to Performance Modelling","author":"J Hillston","year":"1996","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, New York (1996)"},{"key":"33_CR48","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc., Upper Saddle River (1985)"},{"key":"33_CR49","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)"},{"key":"33_CR50","unstructured":"Huang, H., et al.: Capturing the distinction between task and device errors in a formal model of user behaviour 45 (2011)"},{"key":"33_CR51","unstructured":"ISO-8807:1989: Information processing systems - open systems interconnection - LOTOS - a formal description technique based on the temporal ordering of observational behaviour (1989)"},{"key":"33_CR52","unstructured":"Johnson, C.W.: Using assurance cases and boolean logic driven markov processes to formalise cyber security concerns for safety-critical interaction with global navigation satellite systems. ECEASST 45 (2011)"},{"key":"33_CR53","doi-asserted-by":"crossref","unstructured":"Kray, C., Kortuem, G., Kr\u00fcger, A.: Adaptive navigation support with public displays. In: Proceedings of the 10th International Conference on Intelligent User Interfaces, IUI 2005, pp. 326\u2013328. ACM, New York (2005)","DOI":"10.1145\/1040830.1040916"},{"key":"33_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-030-04771-9_18","volume-title":"Software Technologies: Applications and Foundations","author":"S Leriche","year":"2018","unstructured":"Leriche, S., Conversy, S., Picard, C., Prun, D., Magnaudet, M.: Towards handling latency in interactive software. In: Mazzara, M., Ober, I., Sala\u00fcn, G. (eds.) STAF 2018. LNCS, vol. 11176, pp. 233\u2013239. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-04771-9_18"},{"key":"33_CR55","unstructured":"Masci, P., Curzon, P., Blandford, A., Furniss, D.: Modelling distributed cognition systems in PVS. ECEASST 45 (2011)"},{"key":"33_CR56","unstructured":"Masci, P., et al.: On formalising interactive number entry on infusion pumps. ECEASST 45 (2011)"},{"issue":"8","key":"33_CR57","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1109\/TSE.2004.40","volume":"30","author":"G Mori","year":"2004","unstructured":"Mori, G., Paterno, F., Santoro, C.: Design and development of multidevice user interfaces through multiple logical descriptions. IEEE Trans. Software Eng. 30(8), 507\u2013520 (2004). \n                    https:\/\/doi.org\/10.1109\/TSE.2004.40","journal-title":"IEEE Trans. Software Eng."},{"key":"33_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-540-27813-9_45","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496\u2013500. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-27813-9_45"},{"key":"33_CR59","doi-asserted-by":"crossref","unstructured":"Myers, B.A., Rosson, M.B.: Survey on user interface programming. In: Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, CHI 1992, pp. 195\u2013202. ACM, New York (1992)","DOI":"10.1145\/142750.142789"},{"issue":"4","key":"33_CR60","doi-asserted-by":"publisher","first-page":"18:1","DOI":"10.1145\/1614390.1614393","volume":"16","author":"D Navarre","year":"2009","unstructured":"Navarre, D., Palanque, P., Ladry, J.F., Barboni, E.: Icos: a model-based user interface description technique dedicated to interactive systems addressing usability, reliability and scalability. ACM Trans. Comput.-Hum. Interact. 16(4), 18:1\u201318:56 (2009)","journal-title":"ACM Trans. Comput.-Hum. Interact."},{"key":"33_CR61","doi-asserted-by":"crossref","unstructured":"Norman, G., Palamidessi, C., Parker, D., Wu, P.: Model checking the probabilistic $$\\pi $$-calculus. In: Proceedings 4th International Conference on Quantitative Evaluation of Systems (QEST 2007), pp. 169\u2013178. IEEE Computer Society (2007)","DOI":"10.1109\/QEST.2007.31"},{"key":"33_CR62","doi-asserted-by":"publisher","unstructured":"Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: PVSIO-web: a tool for rapid prototyping device user interfaces in PVS. ECEASST 69 (2013). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.69.963","DOI":"10.14279\/tuj.eceasst.69.963"},{"issue":"3","key":"33_CR63","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S Owicki","year":"1982","unstructured":"Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455\u2013495 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"33_CR64","unstructured":"Puschner, P., Burns, A.: A review of worst-case execution-time analyses. Real-time Systems - RTS Jan 1999"},{"key":"33_CR65","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.entcs.2008.03.107","volume":"208","author":"R Ruk\u0161\u0117nas","year":"2008","unstructured":"Ruk\u0161\u0117nas, R., Back, J., Curzon, P., Blandford, A.: Formal modelling of salience and cognitive load. Electr. Notes in Theoret. Comput. Sci. 208, 57\u201375 (2008). Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes in Theoret. Comput. Sci."},{"key":"33_CR66","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2007.01.059","volume":"183","author":"R Ruk\u0161\u0117nas","year":"2007","unstructured":"Ruk\u0161\u0117nas, R., Curzon, P., Blandford, A.: Detecting cognitive causes of confidentiality leaks. Electr. Notes Theoret. Comput. Sci. 183, 21\u201338 (2007)","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"33_CR67","unstructured":"Ruk\u0161\u0117nas, R., Curzon, P.: Abstract models and cognitive mismatch in formal verification. ECEASST 45 (2011)"},{"key":"33_CR68","doi-asserted-by":"publisher","unstructured":"Ruk\u0161\u0117nas, R., Masci, P., Harrison, M.D., Curzon, P.: Developing and verifying user interface requirements for infusion pumps: a refinement approach. ECEASST 69 (2013). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.69.964.945","DOI":"10.14279\/tuj.eceasst.69.964.945"},{"key":"33_CR69","unstructured":"Ryan, M.D., Smyth, B.: Applied pi calculus. In: Formal Models and Techniques for Analyzing Security Protocols. IOS Press (2011)"},{"issue":"1","key":"33_CR70","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2006","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. A. Commun. 21(1), 5\u201319 (2006)","journal-title":"IEEE J. Sel. A. Commun."},{"key":"33_CR71","doi-asserted-by":"crossref","unstructured":"Sannella, D., Wirsing, M.: Specification languages. Algebraic Foundation of Systems Specification. IFIP State-of-the-Art Reports, pp. 243\u2013272, July 1999","DOI":"10.1007\/978-3-642-59851-7_8"},{"key":"33_CR72","unstructured":"SC-205, R.F., 71, E.A.W.G.: Rtca\/do-178c software considerations in airborne systems and equipment certification, December 2011"},{"key":"33_CR73","unstructured":"SC-205, R.F., 71, E.A.W.G.: Rtca\/do-333 formal methods supplement to do-178c and do-278a, December 2011"},{"key":"33_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BFb0031813","volume-title":"Formal Methods in Computer-Aided Design","author":"N Shankar","year":"1996","unstructured":"Shankar, N.: PVS: combining specification, proof checking, and model checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 257\u2013264. Springer, Heidelberg (1996). \n                    https:\/\/doi.org\/10.1007\/BFb0031813"},{"key":"33_CR75","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.entcs.2008.03.108","volume":"208","author":"JL Silva","year":"2008","unstructured":"Silva, J.L., Campos, J.C., Paiva, A.C.: Model-based user interface testing with spec explorer and concurtasktrees. Electr. Notes Theoret. Comput. Sci. 208, 77\u201393 (2008)","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"33_CR76","doi-asserted-by":"publisher","unstructured":"Silva, J.L., Fayollas, C., Hamon, A., Palanque, P., Martiinie, C., Barboni, E.: Analysis of wimp and post wimp interactive systems based on formal specification. ECEASST 69 (2013). \n                    https:\/\/doi.org\/10.14279\/tuj.eceasst.69.967","DOI":"10.14279\/tuj.eceasst.69.967"},{"key":"33_CR77","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/j.entcs.2007.01.062","volume":"183","author":"D Sinnig","year":"2007","unstructured":"Sinnig, D., Chalin, P., Khendek, F.: Towards a common semantic foundation for use cases and task models. Electr. Notes Theoret. Comput. Sci. 183, 73\u201388 (2007)","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"issue":"6","key":"33_CR78","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1080\/01449299508914656","volume":"14","author":"RW Soukoreff","year":"1995","unstructured":"Soukoreff, R.W., Mackenzie, I.S.: Theoretical upper and lower bounds on typing speed using a stylus and a soft keyboard. Behav. Inf. Technol. 14(6), 370\u2013379 (1995)","journal-title":"Behav. Inf. Technol."},{"key":"33_CR79","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1989","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall Inc., Upper Saddle River (1989)"},{"key":"33_CR80","unstructured":"Standardization, I.: ISO 9241\u201311: Ergonomic Requirements for Office Work with Visual Display Terminals (VDTs): Part 11: Guidance on Usability (1998)"},{"key":"33_CR81","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.entcs.2008.03.109","volume":"208","author":"L Su","year":"2008","unstructured":"Su, L., Bowman, H., Barnard, P.: Performance of reactive interfaces in stimulus rich environments, applying formal methods and cognitive frameworks. Electr. Notes in Theoret. Comput. Sci. 208, 95\u2013111 (2008). Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes in Theoret. Comput. Sci."},{"key":"33_CR82","unstructured":"Thimbleby, H., Gimblett, A.: Dependable keyed data entry for interactive systems. ECEASST 45 (2011)"},{"key":"33_CR83","doi-asserted-by":"crossref","unstructured":"Turner, J., Bowen, J., Reeves, S.: Using abstraction with interaction sequences for interactive system modelling: STAF 2018 Collocated Workshops, Toulouse, France, 25\u201329 June 2018, Revised Selected Papers, pp. 257\u2013273, June 2018","DOI":"10.1007\/978-3-030-04771-9_20"},{"key":"33_CR84","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.entcs.2008.03.110","volume":"208","author":"M Westergaard","year":"2008","unstructured":"Westergaard, M.: A game-theoretic approach to behavioural visualisation. Electr. Notes Theoret. Comput. Sci. 208, 113\u2013129 (2008). Proceedings of the 2nd International Workshop on Formal Methods for Interactive Systems","journal-title":"Electr. Notes Theoret. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Formal Methods. FM 2019 International Workshops"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-54994-7_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,14]],"date-time":"2020-08-14T12:48:21Z","timestamp":1597409301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-54994-7_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030549930","9783030549947"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-54994-7_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/?page_id=84","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}