AMC: Verifying User Interface Properties for Vehicular Applications

Kyungmin Lee, Jason Flinn, T.J. Giuli, Brian Noble, and Christopher Peplin.


Vehicular environments require continuous awareness of the road ahead. It is critical that mobile applications used in such environments (e.g., GPS route planners and location-based search) do not distract drivers from the primary task of operating the vehicle. Fortunately, a large body of research on vehicular interfaces provides best practices that mobile application developers can follow. However, when we studied the most popular vehicular applications in the Android marketplace, no application followed these guidelines. In fact, vehicular applications were not substantially better at meeting best practice guidelines than non-vehicular applications.

To remedy this problem, we have developed a tool called AMC that uses model checking to automatically explore the graphical user interface (GUI) of Android applications and detect violations of vehicular design guidelines. AMC is designed to give developers early feedback on their application GUI and reduce the amount of time required by a human expert to assess an application’s suitability for vehicular usage. We have evaluated AMC by comparing the violations that it reports with those reported by an industry expert for 12 applications. AMC generated a definitive assessment for 85% of the guidelines checked; for these cases, it had no false positives and a false negative rate of under 2%. For the remaining 15% of cases, AMC reduced the number of application screens that required manual verification by 95%.