Multitasking is a fundamental mechanism of the Android mobile operating system, which has substantially enhanced user experiences of the system. However, because of its complex nature, this mechanism is infamously hard to understand and is plagued by serious security concerns. In this paper we formalize the semantics of the multitasking mechanism and develop efficient static analysis methods with automated tool supports. For the formalization, we propose an extension of the existing Android stack machine model to capture all the core elements of the mechanism, in particular, the intent flags used in inter-component communication. We define the formal semantics in a succinct and structured way, with some underlying principles identified. Moreover, we pinpoint the discrepancy in the semantics for different Android versions. We also validate the semantics by examining the conformance to the actual behavior of the Android system via exhaustive experiments. For the static analysis, we consider the configuration reachability and stack boundedness problem, designing new algorithms and developing a prototype tool TaskDroid to fully support automated model construction and analysis of Android apps. The experimental results show that TaskDroid is effective and efficient in analyzing Android apps in practice.