近些年来,人工智能的各种计算模型尤其是卷积神经网络得到了快速发展,广泛应用于各种领域中。然而,卷积神经网络训练的过程是基于数理统计的,在理论上具有较大的不确定性,在实际应用中也表现出了一些安全性问题。形式化验证是一种用形式化方法来确定系统是否满足特定性质规约的技术。由于形式化方法是基于数理逻辑的,具有可靠性,所以用形式化验证技术来研究卷积神经网络,将有助于保障卷积神经网络的安全性和提高卷积神经网络模型的可信性。本文立足于形式化验证技术的基础,使用形式化语言MSVL为卷积神经网络开发综合性的建模框架,支持对网络的各级结构和多种行为进行建模,并对多种性质进行验证,旨在改善目前国内外尚缺乏通用的卷积神经网络形式化验证框架的现状。本文提出了一个基于MSVL的卷积神经网络建模框架,支持对于一般的卷积神经网络、全连接神经网络进行建模。本文首先对卷积神经网络的结构进行了构建,将卷积神经网络的结构设计为对应的数据结构,并实现为MSVL中的结构体。其次,本文对卷积神经网络的基本行为进行了构建,将卷积神经网络的基本行为抽象为对应数据结构上的操作,并实现为MSVL中的函数。随后,本文对预测模型、训练模型和验证模块进行开发,设计并实现训练模型和预测模型,形成了可编译运行的卷积神经网络建模框架函数库,为网络级的形式化建模工作提供支持。同时对验证模块进行开发,给出本框架性质验证的流程,为基于本框架的性质验证工作提供了理论支持。最后,在此函数库的基础上,开展了建模实验与验证实验,实验结果表明了本框架的正确性以及在本框架构建的网络模型上进行性质验证的可行性。