Checking activity transition systems with back transitions against assertions

Abstract

The Android system is in widespread use currently, and Android apps play an important role in our daily life. How to specify and verify apps is a challenging problem. In this paper, we study a formalism for abstracting the behaviour of Android apps, called Activity Transition Systems (ATS), which includes back transitions, value assignments and assertions. Given such a transition system with a corresponding Activity Transition Graph (ATG), it is interesting to know whether it violates some value assertions. We first prove some theoretical properties of transitions and propose a state-merging strategy. Then we further introduce a post-reachability graph technique. Based on this technique, we design an algorithm to traverse an ATG that avoids path cycles. Lastly, we also extend our model and our algorithm to handle more complicated problems.