系统建模语言(Systems Modeling Language,SysML)的提出使得模型驱动开发(Model Driven Development,MDD)可以应用于系统工程领域。由于模型驱动开发对自动代码生成的支持,使得目标系统的验证在整个项目开发周期中的位置可以推前到系统的设计阶段进行。在MDD中,模型可分为平台无关模型和平台相关模型,通过验证平台无关模型(Platform Independent Model,PIM)来预览系统的行为功能可以减少系统工程实施的风险。在系统工程领域中,针对平台无关模型进行验证具有重要的意义,合理的平台无关模型可以组织成为高内聚低耦合的可复用组件,提高系统工程的质量和效率,大大减少测试目标系统的时间和开销。系统建模语言是统一建模语言(Unified Modeling Language,UML)的扩展,将会广泛应用到模型驱动开发中,但SysML还在不断完善中,使用原生SysML进行建模不能满足平台无关模型验证的需求,主要原因为:一方面,SysML本身不具备可执行性;另一方面,缺少针对SysML PIM进行设计、分析和验证的工具原型。论文针对目前存在的问题和需求开展了相关研究和实践,主要工作如下:(1)在SysML规范的基础上定义了可执行的平台无关模型。它有一个清晰的模型结构并加入了动作规约语言进行增强,可执行性是进行平台无关模型验证的前提和基础;(2)设计实现了支持基于SysML的可执行平台无关模型的工具原型。用它可以创建和验证可执行的平台无关模型;(3)在可执行模型和工具原型的基础上实现了平台无关模型的验证功能。通过一个具体的模型实例,采用论文中的原型系统进行实验,体现了验证平台无关模型的可行性。