An Operational Semantics for Android Applications

The most common operating system for smart phones, which are among the most common forms of computers today, is the Android operating system. The Android applications are executed on Dalvik Virtual Machines (DVMs) which are register-based, rather than stack-based such as Java Virtual Machines (JVMs). The differences between DVMs and JVMs make tools of programm analysis of JVMs are not directly applicable to DVMs. Operational semantics is a main tool to study, verify, and analyze Android applications. This paper presents an accurate operational semantics AndroidS for Android programming. The set of Dalvik instruction considered in the semantics is designed carefully to capture main functionalities of Android programming and to enable the use of semantics to evaluate method of Application analysis. The semantics also simulates the interaction between users and applications during application executions. The semantics also respects constrains of state changes imposed by the life cycle of Android applications.