An Operational Semantics for Android Applications

Citation:
El-Zawawy, M. A., "An Operational Semantics for Android Applications", 16th International Conference on Computational Science and Its Applications, Beijing, China, July 4-7, 2016.

Date Presented:

July 4-7, 2016

Abstract:

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
\textit{Android}$\mathcal{S}$ 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.

Tourism