模型检验 在模型检验中涉及两种形式说明语言: 性质说明语言用于描述系统的性质 模型描述语言用于描述系统的模型。 模型检验技术用于检验由模型描述语言描述的系 统模型是否满足由性质说明语言描述的系统性质。模型检验 ◼ 在模型检验中涉及两种形式说明语言： 性质说明语言用于描述系统的性质; 模型描述语言用于描述系统的模型。 ◼ 模型检验技术用于检验由模型描述语言描述的系 统模型是否满足由性质说明语言描述的系统性质