目前，嵌入式实时系统的广泛应用使得确保其正确性和可靠性成为当前的研究热点。MARTE（Modeling and Analysis of Real Time and Embedded systems）是UML在嵌入式实时系统领域的建模规范，弥补了UML对嵌入式实时系统领域非功能属性表达能力的不足。MARTE规范采用图形化的方式描述系统，缺乏精确的语义，因此难以直接进行形式化分析和验证。在现代软件系统开发过程当中，还经常会要求在某些限定的时间约束之下，对系统的输入数据以及系统内部状态之间的变迁进行相应的处理，最后给出对应的输出数据，因此对数据变量进行处理也十分必要。形式化方法作为一种以数学为基础的方法，能够清晰、精确、抽象、简明地规范和验证软件系统及其性质，极大地提高软件的安全性和可靠性。本文通过将MARTE模型转换到形式化模型进行验证，以确保软件的可信度。首先，对MARTE进行扩充，将MARTE与Z语言相结合提出一种描述带有数据约束的嵌入式实时系统规范Z-MARTE。然后，提出一种描述带数据约束实时系统的形式化规范基于连续时间的ZIA规范，并将Z-MARTE转换为基于连续时间的ZIA规范模型，这样在实现了对基于连续时间的ZIA模型的模型检测时，也就实现了对Z-MARTE的模型检测。本文最后给出基于连续时间的ZIA规范模型的模型检测算法，并通过一个实例验证，阐述了文章方法的可行性和有效性。另外，由于传统的ZIA没有刻画系统概率方面的能力，因此文章在传统的ZIA上扩展了概率性质提出一种针对概率系统的ZIA规范PZIA，使之不仅能够刻画系统的行为和状态，还能够刻画系统的概率性质。对于传统的时序逻辑如计算树逻辑CTL和概率计算树逻辑PCTL来说，尽管这些逻辑很强大，但是只能反映系统的时序性质，为了解决这些局限性，本文提出一个新的形式化语言来表达度量性质查询，同时保留表达时序性质的能力。然后文章给出针对概率系统度量性质的检测算法并通过实例说明本文提出的方法可行有效。