对象约束语言OCL的出现,为精确化模型奠定了基础。而随着模型在软件开发中的地位越来越重要,如何对施加在模型上的OCL约束进行验证从而提高模型的准确性,保证模型的一致性工作显得极其重要。主流的建模工具不支持OCL约束的定义,或者在代码生成的过程中忽略了施加在模型上的约束,少数支持约束代码生成的工具缺乏完整的验证机制,需要用户手动编写验证代码相关调用,这就带来了模型间的不一致性问题。在软件系统规模不断增大和复杂化的背景下,这些建模工具已经不能完全适应用户的需求。针对这样的问题,本文提出了一种基于OCL的约束验证框架。框架通过定义约束提供了更加精确的模型,并且通过模型转换的方法生成模型代码和验证器,为用户提供最大的方便,减少了模型与所生成代码在软件生命周期中的一致性问题,提高了软件开发的效率。具体而言,本文的工作包括以下几个方面：1)基于Ecore元模型中的EAnnotation元素,提出了一种模型约束的定义方法,使得用户可以在开发模型的同时施加模型约束,方便用户的同时,丰富了模型的语义,提高了模型的准确性。2)通过为上述包含约束信息的模型定义JET(Java Emitter Templates)代码生成模板,在生成模型代码的同时,为模型生成相应的验证器,将验证器注册在模型代码中完成模型实例的验证工作。在代码层面实现了模型代码与验证逻辑的松耦合,保证了模型和代码之间的一致性,同时也提高了开发效率。3)基于Eclipse中的图形编辑框架GEF,设计并实现了一个基于上述框架的体系结构开发环境——Artemis-EIDE,工具在上述框架中定义了软件体系结构中的基本模型和模型约束,使用框架所生成的模型代码以及验证器代码,根据现有的可视化建模框架GEF完成部分定制,实现了软件体系结构的建模和验证环境,以此探索和展示框架在模型实例验证支持上的特点和潜在优势。