Separation logic for states dependencies in life cycles of android activities and fragments

Abstract

Millions of smart phones are run by Android, the most common operating system for mobile devices. Main component of Android is applications providing most functionalities of Android smart devices. These applications include e-mail client, entertainment, educational, news, banking, maps, and contacts applications. Testing and verifying Android applications is an important direction of research. This paper presents a separation logic for state transitions of activities and fragments (important components of applications) during their life cycles. The logic considers the necessary coordinations between the state transitions in the two life cycles. The logic is a good tool to verify and test applications against various issues including security ones.