形式化方式包括了形式规范和设计验证两个方面，它的目的是以数学的方式来对系统进行描述，为保证软件的可靠性提供条件。在现代软件系统开发过程当中，经常会要求在某些限定的时间约束之下，对系统的输入数据进行相应的处理，以及系统内部所进行的状态之间的变迁，最后给出对应的输出数据。本文的主要工作如下：本文首先介绍了一种结合接口自动机（Interface Automata）和Z语言的规范ZIA以及ZIAs之间的精化关系。然后研究了MARTE（Modeling and Analysis of Real-Time andEmbedded Systems），它在UML的基础上对于时间以及其他方面进行了一定的扩充。MARTE定义了基于模型的实时和嵌入式系统描述的基础。本文详细描述了MARTE中的一些基本和核心概念。然后给出了一种基于离散时间的ZIA模型规范（DT-ZIA），它不仅能够描述某些实时系统中针对在离散时间下的时间约束的要求，同时能够对系统的数据处理和状态变迁进行精确的表达。接着是MARTE的六元组表示，再接着是MARTE到DT-ZIA的转换方法。最后我们给出了在有限定义域上的ZIAs精化检测算法（包括算法的数据结构和流程图）、面向带有数据约束的实时系统的时序逻辑和在有限定义域上的DT-ZIA模型检测算法（包括实现类图和流程图）以及两个算法的实例验证。