The Modeling and Verification of Trainify

(Tennis App)


  • Kainat Fatima National University of Science and Technology, NUST
  • Sidra Sultana
  • Jawad Ali Abbasi
  • Muhammad Talha Khalid



Uppaal, System Verification, System Modeling, Tennis training, Time and Speed


Safety and correctness can be assured in a system by applying numerous testing techniques. We have used formal modeling and verification for our work given it allows us to thoroughly test the app by going through all its real time aspects. In this paper we have modelled and verified a tennis training app, Trainify, to prevent wrong play in tennis and to also ensure that our tennis athletes or beginners do not hurt themselves in the process of learning or playing tennis. We found several modules which could compromise the safety pf the players and created their modules in Uppaal by modelling and then verified them using Uppaal’s verifier feeding it the different properties to be tested to ensure no such bad state occurs for our users. A detailed simulation of the model is presented and described.




How to Cite

Kainat Fatima, Sidra Sultana, Jawad Ali Abbasi, & Muhammad Talha Khalid. (2022). The Modeling and Verification of Trainify: (Tennis App). International Journal of Emerging Multidisciplinaries: Computer Science & Artificial Intelligence, 1(2), 26–34.



Research Article