随着软件规模的日益增大、软件复杂度的日渐增加,大型系统的开发往往是由多个不同专业领域、具有不同职能的团队相互协作完成。以往的协同过程基本上是在各自的设备上进行开发与调试,通过人员沟通、现场集成、联调测试等方式进行开发过程的协同。随着软件不断向复杂化、规模化与开放化的趋势发展,原有的协同方式已经无法满足现有软件协同开发的需求。因此,研究软件协同建模与模型验证技术具有十分重要的意义。论文主要的研究工作以及成果如下:（1）为了在软件设计阶段更好地支持协同建模,提出了一种结合模型驱动与软件协同的模型组装与更新方法MCUM（Model Combination and Update Method）。MCUM在元模型的基础上添加了协同关系与更新操作,通过扩展的语义能够更好地对模型进行校验,并且提高协同建模效率。还设计了基于模型驱动的模型组装与更新框架MCUF（Model Composition and Update Framework）,该框架可将局部模型组装为全局模型并进行更新。最后,通过一个实例演示了该方法模型组装与更新的过程,验证了其有效性与正确性。针对模型组装过程中元素丢失导致的模型不完整问题,根据协同关系设计了模型完整性校验算法,该算法通过局部模型之间的协同关系判断元素是否发生丢失。针对模型更新过程中操作冲突导致的模型不一致问题,根据更新操作设计了模型一致性校验算法,该算法通过更新操作之间的关系检测是否发生冲突。（2）为了在模型验证阶段更好地支持形式化方法,提出了一种结合半形式化与形式化的模型转换与验证方法MTVM（Model Transformation and Validation Method）。MTVM在Z语言的基础上结合UML静态模型建立了ZClass模型,在时间自动机的基础上结合UML动态模型建立了TState模型。还设计了基于模型驱动的模型转换与验证框架MTVF（Model Transformation and Validation Framework）,该框架可将半形式化的UML模型转换为形式化模型并进行模型验证。最后,通过一个实例演示了该方法模型转换与验证的过程,验证了其有效性与正确性。针对UML静态模型缺少操作规约的问题,设计了类图到ZClass模型的映射规则与转换算法,并可对模型的静态结构进行可用性验证。针对UML动态模型缺少时间约束的问题,设计了状态图到TState模型的映射规则与转换算法,并可对模型的动态行为进行实时性验证。（3）在上述研究成果的基础上,基于Eclipse开源框架,设计并初步实现了基于模型驱动的协同建模与模型验证平台。该平台包括三个子系统:协同建模模型组装与更新子系统、UML静态模型转换与验证子系统和UML动态模型转换与验证子系统。平台功能和性能测试结果表明,该平台能够在较小的时间开销下进行协同建模与模型验证,可有效地提高软件的开发效率。