王立杰，刘昌禄，俞烈彬

(江苏自动化研究所，江苏 连云港 222006)

嵌入式系统是一种嵌入到具体设备中，对性能、成本、功耗等有严格要求的专用计算机系统，目前已经广泛应用于军事、通讯、医疗、交通等行业中。运行时系统功能的失效或者违反安全性、可靠性、实时性等非功能属性都将导致灾难性的后果［1］。因此，提高软件可信性成为嵌入式软件开发领域的重要课题。

MARTE(Modeling and Analysis of Real Time and Embedded systems)是UML在嵌入式实时系统领域的建模规范［2］，弥补了UML对嵌入式实时领域的非功能属性的表达能力的不足。UML/MARTE规范采用图形化的方式描述系统，缺乏精确的语义信息，因此难以直接进行一致性验证。形式化方法提供了一种严格精确的数学方法，通常被用于软件设计阶段，分析系统的可靠性［3］。Ahmed M.Mostafa等提出使用Z形式化UML用例图、类图、状态图等［4］。张天等利用AMMA平台，在元模型层定义了MARTE到FIACRE的映射关系，完成了异构转换［5］。Soon-Kyeong Kim and David Carrington提出了元建模方法完成从UML图到Object-Z的转换，两种语言定义在元模型层次，保证了转换的精确性，完整性和一致性［6］。目前研究者对UML的形式化进行了多方面的研究，并考虑MARTE与嵌入式系统的其它建模语言进行转换或集成，但对于MARTE模型的形式化基础研究的还比较少。

本文首先建立了扩展的Object-Z的元模型，以方便描述嵌入式时间和资源非功能属性。然后在MDA框架下分别定义MARTE静态结构图，动态行为图和时间资源非功能属性到Object-Z语义的转换规则，实现MARTE模型到Object-Z规约之间的转换。从而可以根据Object-Z规范及其推理技术对MARTE模型进行形式化的验证。……