论文部分内容阅读
非形式化／半形式化模型到形式化模型之间的转换是当前软件工程领域的研究热点。根据异构模型转换，提出了基于MDA的MARTE模型到Object-Z规约之间的转换方法。针对Object-Z在实时领域表达能力不足的问题，首先扩展Object-Z元模型；然后在MDA的元元模型体系下，定义了MARTE元模型和扩展的Object—Z元模型之间的转换规则。MARTE模型可以重用这些转换规则以实现到Object-Z形式化描述之间的转换，进而可以对模型进行形式化验证；最后通过一个实例使用该方法完成模型转换，具体说明了转换规则