Conference Proceedings

Verifying nondeterministic processes driven by broadcasts on Android

C Luo, X Ma, Y Tian, J Goncalves, E Velloso, V Kostakos

2019 IEEE 3rd Information Technology, Networking, Electronic and Automation Control Conference (ITNEC) | IEEE | Published : 2019

Abstract

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. W..

View full abstract

Grants

Awarded by NSFC


Awarded by National Science Foundation of Shanghai Municipal


Awarded by National Natural Science Foundation of China


Awarded by Ningxia High Education research fund


Awarded by fund of Ningxia High Education Construction of First-Class Disciplines (Education)


Awarded by Key Research and Development (Science and Technology Support Program) Program of Ningxia Province


Awarded by undergraduate teaching project of Ningxia High Education


Funding Acknowledgements

This work is supported by NSFC grant 11671258, 11771280, National Science Foundation of Shanghai Municipal (17ZR1415400), National Natural Science Foundation of China under grant No.11361046, Ningxia High Education research fund with grant No.NGY2017180, undergraduate teaching project of Ningxia High Education with grant No.NXJG2016060, and the fund of Ningxia High Education Construction of First-Class Disciplines (Education) with grant No.NXYLXK2017B11, The Key Research and Development (Science and Technology Support Program) Program of Ningxia Province No.2018BEE03025, 2018BEE03026.