FMitF: Formal Verification of Accessibility

FMITF：可访问性的形式验证

• 批准号: 1836813
• 负责人: Michael Ernst
• 金额: $ 73.81万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-01-01 至 2022-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1836813&HistoricalAwards=false
• 关键词: FMitF; Formal; Verification; Accessibility

Most of the web is not designed for accessibility for the nearly one billion people that have a disability such as blindness, low vision, motorphysical impairments, or dyslexia, and no comprehensive, precise verification tools currently exist for checking accessibility. Existing testing tools are limited, imprecise, and incomplete, and even when they are used, they give guarantees only about one particular web browser configuration such as window size, default fonts and colors. This project aims to enable the formal verification of web accessibility. The research to be pursued involves the automatic identification of a broader class of accessibility problems that is currently possible and is intended to give guarantees of absence of such problems for all possible web browser configurations. The software tools developed in this project are intended to give web developers and content producers targeted, concrete feedback on who is affected by an accessibility issue, and why, and how to fix any problems. The project develops a user interface logic for specifying accessibility properties, and formalizes a large fragment of browser rendering algorithms using novel finitization reductions. The project builds software tools that translates web pages, accessibility rules, and the browser algorithm to quantifier-free linear real arithmetic, using an SMT solver to verify it or produce a concrete, inaccessible rendering of the webpage. To make the results of these verifications useful and usable to developers, content producers, and web users, the investigators develop new classes of concrete, comprehensible, and actionable warning explanations and new techniques for patching accessibility at run time. To evaluate all of this work, the project is partnering with Adobe, Instructure, and Wikimedia.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

大多数网络并不是为近十亿人（例如失明，低视力，摩托车障碍或阅读障碍）的十亿人设计的，并且目前没有全面，精确的验证工具可用于检查可访问性。现有的测试工具有限，不精确和不完整，即使使用它们，它们也只能保证一种特定的Web浏览器配置，例如窗口尺寸，默认字体和颜色。该项目旨在使网络可访问性进行正式验证。要进行的研究涉及自动识别当前可能发生的更广泛的可访问性问题，并旨在保证所有可能的Web浏览器配置都没有此类问题。本项目开发的软件工具旨在为Web开发人员和内容生产者提供针对性的，具体的反馈，内容涉及谁受到可访问性问题的影响，以及为什么以及如何解决任何问题。 该项目开发了用于指定可访问性属性的用户界面逻辑，并使用新颖的缩减降低了浏览器渲染算法的大量片段。该项目构建了将网页，可访问性规则和浏览器算法转换为无量词的线性真实算术算术的软件工具，并使用SMT求解器验证它或生成网页的具体，无法访问的渲染。为了使这些验证的结果对开发人员，内容生产者和网络用户有用，并且可以在运行时开发新的具体，可理解和可行的警告说明和新技术，以在运行时间修补可访问性。为了评估所有这些工作，该项目正在与Adobe，“指导”和Wikimedia合作。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛的影响评估标准通过评估来获得支持的。

项目成果

Anticipate and Adjust: Cultivating Access in Human-Centered Methods

预测和调整：培养以人为本的方法的可及性

• DOI: 10.1145/3491102.3501882
• 发表时间: 2022
• 期刊: CHI '22: Proceedings of the 2022 CHI Conference on Human Factors in Computing Systems
• 作者: Mack, Kelly;McDonnell, Emma;Potluri, Venkatesh;Xu, Maggie;Zabala, Jailyn;Bigham, Jeffrey;Mankoff, Jennifer;Bennett, Cynthia
• 通讯作者: Bennett, Cynthia

PSST: Enabling Blind or Visually Impaired Developers to Author Sonifications of Streaming Sensor Data

PSST：使盲人或视障开发人员能够创作流传感器数据的声音

• DOI: 10.1145/3526113.3545700
• 发表时间: 2022
• 期刊: UIST '22: Proceedings of the 35th Annual ACM Symposium on User Interface Software and Technology
• 作者: Potluri, Venkatesh;Thompson, John;Devine, James;Lee, Bongshin;Morsi, Nora;De Halleux, Peli;Hodges, Steve;Mankoff, Jennifer
• 通讯作者: Mankoff, Jennifer

Computing Students' Learning Difficulties in HCI Education

计算学生在人机交互教育中的学习困难

• DOI: 10.1145/3313831.3376149
• 发表时间: 2020
• 期刊: ACM SIGCHI Conference on Human Factors in Computing Systems (CHI
• 作者: Oleson, Alannah;Solomon, Meron;Ko, Amy J.
• 通讯作者: Ko, Amy J.

Teaching Accessibility: A Design Exploration of Faculty Professional Development at Scale

教学可及性：大规模教师专业发展的设计探索

• DOI: 10.1145/3287324.3287399
• 发表时间: 2019
• 期刊: ACM Technical Symposium on Computer Science Education (SIGCSE
• 作者: Kawas, Saba;Vonessen, Laura;Ko, Andrew J.
• 通讯作者: Ko, Andrew J.

Teaching Inclusive Design Skills with the CIDER Assumption Elicitation Technique

使用 CIDER 假设启发技术教授包容性设计技能

• DOI: 10.1145/3549074
• 发表时间: 2022
• 期刊: ACM Transactions on Computer-Human Interaction
• 影响因子: 3.7
• 作者: Oleson, Alannah;Solomon, Meron;Perdriau, Christopher;Ko, Amy J.
• 通讯作者: Ko, Amy J.