{"id":{"repo_id":"buffalo","oai_identifier":"oai:ubir.buffalo.edu:10477/78641"},"canonical_url":"https://search.dev.ndltd.org/etd/buffalo/oai:ubir.buffalo.edu:10477/78641","repository":{"repo_id":"buffalo","name":"Buffalo","base_url":"https://ubir.buffalo.edu/oai/request"},"display":{"title":"Formal Methods for User Experience Evaluation and Testing","abstract":"Ph.D.","abstract_html":"Ph.D.","abstract_has_math":false,"creators":["Li, Meng"],"institution":"State University of New York at Buffalo","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Bolton, Matthew","Industrial and Systems Engineering"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-10-26T02:57:18Z","date_published":"2018-10-26T02:57:18Z","updated_at":"2026-07-27T19:05:14Z","subjects":["industrial engineering"],"languages":["eng"],"rights":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10477/78641","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Bolton, Matthew","Industrial and Systems Engineering"]},{"key":"dc:creator","label":"Author","values":["Li, Meng"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2018-10-26T02:57:18Z","2018","2018-08-10 17:48:01"]},{"key":"dc:publisher","label":"Institution","values":["State University of New York at Buffalo"]},{"key":"dc:type","label":"Dc Type","values":["Text","Dissertation"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["industrial engineering"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/10477/78641"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Ph.D.","Human-machine systems have been expanding their roles in industry and in society. However, the growing complexity of interactive systems requires more and more efforts to ensure reliability, usability, and satisfying user experience. Testing is an effective approach for finding and correcting discrepancies between intended and actual system behavior as well as the ability to find usability problems unanticipated at design time. Testing is often regarded as the most intellectual-demanding, time-consuming, and expensive part of software and system development processes. It can thus be difficult (if not impossible) for testers to anticipate all of the system conditions that need to be evaluated. This is especially true of human-machine systems. This is because the human operator (who is attempting to achieve his or her task goals) is an additional concurrent component to the system, and one whose behavior is not governed by the implementation of designed system elements.To address these issues, researchers have developed approaches to automating the generation of test cases. Among these are formal methods: mathematically based languages, techniques, and tools for the modeling, specification, and analysis of systems. These support model-based approaches for creating tests that are efficient and provide guarantees about their completeness (with respect to the model). In particular, model checking can be used for automated test case generation. In this, efficient and exhaustive search techniques parse models of a system to satisfy specified coverage criteria (descriptions of the system conditions the test cases should encounter during execution).In this dissertation, I introduce a new method for automatically generating test cases for human-machine systems. This uses a combination of human task behavior models, decision models, and system models. With a given formal coverage criterion (based on the system and task models), tools based on model checking are used to automatically generate test sequences from the formal model. The test cases are guaranteed to be complete with respect to the coverage criteria. Using different human decision models, based on utility theory, test cases can be designed to replicate interaction scenarios representative of different types of users. Tests generated using my approach can be used to validate that system implementations satisfy properties proved about the formal model. They can also be used to gain insights into system usability that would not have been possible to include in a formal system model. Finally, the novel inclusion of human decision modeling enables generated tests to represent interaction scenarios that will give analysts and testers insights into different types of users’ experiences.In this dissertation, I describe my method and demonstrate its capabilities with two applications: a pod-based coffee machine and a smart thermostat. I also discuss my research contributions and explore future research possibilities."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Formal Methods for User Experience Evaluation and Testing"]}]}],"canonical_facts":{"dc:contributor":["Bolton, Matthew","Industrial and Systems Engineering"],"dc:creator":["Li, Meng"],"dc:date":["2018-10-26T02:57:18Z","2018","2018-08-10 17:48:01"],"dc:description":["Ph.D.","Human-machine systems have been expanding their roles in industry and in society. However, the growing complexity of interactive systems requires more and more efforts to ensure reliability, usability, and satisfying user experience. Testing is an effective approach for finding and correcting discrepancies between intended and actual system behavior as well as the ability to find usability problems unanticipated at design time. Testing is often regarded as the most intellectual-demanding, time-consuming, and expensive part of software and system development processes. It can thus be difficult (if not impossible) for testers to anticipate all of the system conditions that need to be evaluated. This is especially true of human-machine systems. This is because the human operator (who is attempting to achieve his or her task goals) is an additional concurrent component to the system, and one whose behavior is not governed by the implementation of designed system elements.To address these issues, researchers have developed approaches to automating the generation of test cases. Among these are formal methods: mathematically based languages, techniques, and tools for the modeling, specification, and analysis of systems. These support model-based approaches for creating tests that are efficient and provide guarantees about their completeness (with respect to the model). In particular, model checking can be used for automated test case generation. In this, efficient and exhaustive search techniques parse models of a system to satisfy specified coverage criteria (descriptions of the system conditions the test cases should encounter during execution).In this dissertation, I introduce a new method for automatically generating test cases for human-machine systems. This uses a combination of human task behavior models, decision models, and system models. With a given formal coverage criterion (based on the system and task models), tools based on model checking are used to automatically generate test sequences from the formal model. The test cases are guaranteed to be complete with respect to the coverage criteria. Using different human decision models, based on utility theory, test cases can be designed to replicate interaction scenarios representative of different types of users. Tests generated using my approach can be used to validate that system implementations satisfy properties proved about the formal model. They can also be used to gain insights into system usability that would not have been possible to include in a formal system model. Finally, the novel inclusion of human decision modeling enables generated tests to represent interaction scenarios that will give analysts and testers insights into different types of users’ experiences.In this dissertation, I describe my method and demonstrate its capabilities with two applications: a pod-based coffee machine and a smart thermostat. I also discuss my research contributions and explore future research possibilities."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/10477/78641"],"dc:language":["eng"],"dc:publisher":["State University of New York at Buffalo"],"dc:rights":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."],"dc:subject":["industrial engineering"],"dc:title":["Formal Methods for User Experience Evaluation and Testing"],"dc:type":["Text","Dissertation"]},"updated_at":"2026-07-27T19:05:14Z"}