Verification of Mobile SMS Application with Model Checking Agent

In years, the evolution of mobile SMS (short message service) application is become one of the high demand technology which introduced the fast service and cost saving. So due to this, SMS become a platform for developing information services in order to enhance the way of conventional system been conducted. However, at certain limitation this increasing convergence has effected the performance of information services when the system face the uncertainties and unprecedented risk. System has become unstable and prone to errors, which consequently effect the user satisfaction. Therefore, the trusted model system is extremely important to build the dependable software system. So, this paper propose a model checking agent approach to handle the verification and validation of mobile SMS application in order to ensure that the design of the system is correct. First, we present the architecture of model checking agent in the test case study to verify the SMS message that received by the system. Then, we formalize the design into PROMELA specification for SPIN model checker. Result from the SPIN model checker is able to determine whether the model is satisfy the properties of the requirement stated or could be otherwise. This model checking agent proposed is focused on the verification towards the mobile SMS application.