DefinePK

Abstract

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.