Analyzing Lifecycle Behavior of Android Application Components

An app is an Android application to have interactions with users. If it does not satisfy conditions posed by the pre-defined lifecycle behavior, the whole system often results in consuming unexpectedly large amount of computing resources. Understanding the lifecycle behavior is mandatory, but the explanations on the lifecycle behavior in the standard technical document are narrative and under-constrained. They are not precise enough. This paper presents Alloy-based descriptions of the lifecycle behavior. They can be served as precise and formally analyzable technical documents. Checking different scenarios using the scope-bounded analysis technique helps users and programmers grasp a consistent view of the behavior.