| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | August 10, 2018 |
| Latest Amendment Date: | June 10, 2022 |
| Award Number: | 1836813 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Pavithra Prabhakar
CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | January 1, 2019 |
| End Date: | December 31, 2022 (Estimated) |
| Total Intended Award Amount: | $738,125.00 |
| Total Awarded Amount to Date: | $786,125.00 |
| Funds Obligated to Date: |
FY 2019 = $16,000.00 FY 2021 = $16,000.00 FY 2022 = $16,000.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
4333 BROOKLYN AVE NE SEATTLE WA US 98195-1016 (206)543-4043 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
Box 352350 Seattle WA US 98195-2350 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
Software & Hardware Foundation, FMitF: Formal Methods in the F |
| Primary Program Source: |
01001819DB NSF RESEARCH & RELATED ACTIVIT 01001920DB NSF RESEARCH & RELATED ACTIVIT 01002122DB NSF RESEARCH & RELATED ACTIVIT |
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
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.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
The team developed the first toolkit that equips blind and visually impaired (BVI) developers with the tools to create accessible data displays. Called PSST (Physical computing Streaming Sensor data Toolkit), it enables BVI developers to understand the data generated by sensors from a mouse to a micro:bit physical computing platform. By assuming visual abilities, earlier efforts to make physical computing accessible fail to address the need for BVI developers to access sensor data. PSST enables BVI developers to understand real-time, real-world sensor data by providing control over what should be displayed, as well as when to display and how to display sensor data. PSST supports filtering based on raw or calculated values, highlighting, and transformation of data. Output formats include tonal sonification, non-speech audio files, speech, and SVGs for laser cutting. We validated PSST through a series of demonstrations and a user study with BVI developers.
Additionally, this grant supported extensive studies including understanding engineers? baseline familiarity with accessibility techniques. This is critical for verifying accessibility: we must ensure that the engineers who triage, diagnose, and repair accessibility defects have sufficient knowledge to do so. In a field study with more than two dozen developers highly experienced with software engineering but inexperienced with accessibility, we found that many engineers avoid prioritizing accessibility defects because they do not feel confident estimating the severity of accessibility problems, do not feel confident either formally or informally verifying that they?ve resolved a problem, and in many cases, make assumptions that accessibility problems are not problems.
The team also explored how programming language design itself can help or hinder formal verification of accessibility. In traditional languages, much of the information necessary for accessibility is often discarded at compile or runtime for the sake of efficiency. The team explored the design of programming languages that incorporate accessibility in the language itself, including extensive provenance information that allows all aspects of program evaluation to be described as text, as well as enabling extensive formal static analysis of what accessibility information is missing. Our prototype, a language designed for creative expression with typography, provides a promising platform for enabling formal verification of accessibility.
Finally, the team also investigated how program equivalence techniques can be enhanced, and even automatically extended, with the goal of ensuring that software capabilities are maintained across different interaction models. Such high-level reasoning is difficult in complex software environments where functionality may be accessed via different modalities. This grant helped establish the foundation to automatically infer behavioral equivalences between different operations so that, if one method of computing some desired result is not available under a certain mode, the user may be able to apply another equivalent set of operations to achieve an equivalent result.
Last Modified: 04/07/2023
Modified by: Zachary Tatlock
Please report errors in award information by writing to: awardsearch@nsf.gov.
