Verifying nondeterministic processes driven by broadcasts on Android

Broadcasts in Android facilitate inner-process and inter-process communications. Although broadcasts enable high scalability and loose coupling in achieving collaboration among system components, there is no support for developers to verify the correctness of broadcast-driven nondeterministic processes. To overcome this challenge, we propose a verification approach for systems driven by all the four types of Android broadcasts. Our approach uses the PROMELA language to model broadcast senders and receivers, with regards to unique features of each broadcast type. Based on our design of initialisation procedures, developers can verify properties of their systems using the SPIN model checker. We evaluate our approach in a case study on an example system. Results show that our approach can effectively conduct verification in terms of safety, liveness and never claims with limited computing resources.