Verification Of UML Activity Chart Using SPIN

With the development of computer technology, the extensive application of software system, the portability, serviceability and cooperation ability of software system become more and more important. MDA (Model Driven Architecture) which take the model as the key of software developing, is a new technology to resolve these problems. PIM(Platform Independent Model), which is set up with UML activity chart is one of the core of the model. But majority of the Models lack for verification of correction or only check the local expressions during the modeling process, so causing the existence of the deadlock, live-lock and other bugs in the model. It causes many problems directly during the dynamic execution of the model. So it is important that model and verify the model before running. on the support of National High-tech R&D Program, Model-driven high-reliability software development technology, I was as a team member to achieve the UML activity diagram of the automated verification.Model checking, as one of the formal methods has many good advantages, such as automatism and providing the violate example. Recent years, model checking has been popular in verifying UML model. Model checker SPIN is developed by Bell Lab and it can be used to analysis and verify software.Based on the model checker SPIN, this paper is analysis and verify the PIM model of UML activity chart. Firstly, on the base of PIM model set up by UML activity chart, covert the UML activity chart into PROMELA model which can be identified by model check tool SPIN, then combine the verification function of SPIN to carry on a verification to the activity chart, and get the verification information, and can carry on dynamic state emulation to the activity chart under the situation that come amiss.