Applying Model Checking Agent for Error Detecting in SMS using Formal Method

Abstract

Considering the current mobile driven evolution, entrepreneurs' are eager to increase the performance of their business services. They want an efficient system that able to manage the finances, transactions and communications in a dependable and secure way. Therefore, a method that avoids technical errors, software bugs and requirements misunderstanding is needed. This paper presents a model checking agent approach for error detection in SMS (Short Message Service) application using SPIN. We focus on the behavior and the property verification using model checking agent to support the quality of services for system performance. The motivations of this work are: (1) enhancing the architecture of distributed system into agent based and translating it into formal specification; (2) proving the generated specifications using XSpin model checker. The aim of this approach is to provide a satisfying and verified system design through the modeling of model checking agent with an existed case study.