随着模型驱动技术在软件开发中的广泛应用,以UML为代表的大量可视化建模语言不断涌现,但它们中的大部分目前还没有严格的形式语义,所建立的模型存在很多潜在不一致性等问题,大大影响了系统的可信性。因此如何为模型驱动工程领域的非(半)形式模型提供有效的验证和仿真手段一直备受学术界和工业界的普遍关注。本文针对目前实时嵌入式领域广泛应用的可视化建模语言及规范UML-MARTE和SysML进行了深入研究,通过基于MDE的模型转换技术将这两类模型转换到形式系统及仿真平台上,从而利用形式验证支持工具和仿真平台对系统模型进行一定的验证和仿真支持,进而达到在系统设计的早期就能够灵活地检查和验证系统的性质。具体地说,我们的工作集中在以下几个方面：本文首先研究了基于MDE的SysML状态机图到时间自动机的两种转换方法及SysML顺序图到时间自动机的转换方法。对于转换结果,我们利用已有的时间自动机验证工具对其进行验证,从而间接地利用形式模型及工具解决了验证SysML状态机图模型和顺序图模型的问题。其次,本文研究了基于MDE的模型到仿真代码生成技术。在这一部分,我们首先研究了MARTE模型和SystemC模型之间的语义对应关系,然后基于QVT和ATL等主流转换语言开发相应的模型转换规则,并基于相应的执行引擎实现对应的模型转换,从而将MARTE模型映射到仿真平台,以获得仿真平台对系统模型动态仿真验证的支持。最后,在进行了如上转换工作的基础上,我们针对QVT和ATL两类主流模型转换语言,总结和比较了它们在不同转换场景中的优缺点,从而形成了我们对声明式转换规则的图形化定义,以提高模型转换规则的易理解性。