FMitF: Formal Verification of Accessibility

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

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.