基于MDA的电信业务开发过程中的模型验证研究

Service creation based on MDA is the current research focus on software engineering. It makes great significance to introduce this service creation approach into the telecommunications. Model checking is one of the very important part of the MDA development process, which relates to whether the model meet the requirements and the auto-generated code is available. But MDA is merely a framework and standards, different fields according to the characteristics of businesses in their respective put forward their concrete realization. And currently popular model checking tools and research can not meet the characteristics of the services in telecom area. This paper propose model checking methods and rules in the process of development of the telecommunication services based on MDA, describes these validation rules from the formalize point of view, and gives the corresponding algorithm for model checking.