Probabilistic User Models for the Verification of Human-Computer Interaction

Markus Wagner


We present a method that allows the formalization, analysis, and 
verification of probabilistic human-computer interaction (HCI) with the 
support of model checking tools. Based on a method for the formalization 
of HCI under security aspects, our method allows us to model 
probabilistic user behavior as well as to offer support for the 
computation of the interaction’s cost. It enables us to verify 
quantitative aspects of the interaction and to answer questions like 
“what is the probability that the user will send confidential 
information to unauthorized individuals” and “will the user (on average) 
be able to send the email within a given amount of time?”