Verification of the Environment Information System Based on Model Checking
Download as PDF
Yongbo Wang, Wei Zhang
With the development of 4G and 5G mobile communication technology, using mobile phone to pay for goods and services has become a very popular application. The traditional forms of payment cannot be applied in e-commerce environment. This paper employs model checking method to verify the security and reliability of the Environment Information Systems. A PROMELA model for the System is present. As an important part of the modeling methodology, the Environment Information System is translated into a simpler model that nevertheless preserves all the essential behavior to be verified. It also proposes initial results on the actual verification of the Environment Information System using SPIN. The result of this work is a complete procedure for the modeling and verification of the Environment Information System.
Environment information systems, model checking, linear temporal logic.