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.

大多数网站都不是为近10亿失明、视力低下、肢体运动障碍或阅读障碍等残疾人的无障碍而设计的，目前没有全面、准确的核实工具来检查无障碍。现有的测试工具是有限的、不精确的和不完整的，即使在使用它们时，它们也只能保证一个特定的Web浏览器配置，如窗口大小、默认字体和颜色。该项目旨在实现对网站无障碍的正式核查。将进行的研究涉及自动识别目前可能出现的更广泛类别的可访问性问题，目的是保证所有可能的网络浏览器配置都不会出现这种问题。在这个项目中开发的软件工具旨在为网络开发人员和内容制作者提供有针对性的具体反馈，说明谁受到可访问性问题的影响，以及为什么以及如何解决任何问题。该项目开发了用于指定可访问性属性的用户界面逻辑，并使用新的终结化缩减来形式化大片段的浏览器呈现算法。该项目构建了软件工具，将网页、可访问性规则和浏览器算法转换为无量词的线性实数运算，使用SMT解算器进行验证，或生成具体的、不可访问的网页渲染。为了使这些验证的结果对开发人员、内容制作者和Web用户有用和可用，调查人员开发了新的具体、可理解和可操作的警告解释类别，以及用于在运行时修补可访问性的新技术。为了评估所有这些工作，该项目与Adobe、InStructure和维基媒体合作。该奖项反映了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.