一种基于MSVL的神经网络系统的建模和验证方法

作者:王小兵; 杨坤; 段振华; 赵亮; 田聪; 张南
来源:2019-06-26, 中国, CN201910563393.X.

摘要

本发明属于系统形式化建模与验证技术领域,公开了一种基于MSVL的神经网络系统的建模和验证方法。采用MSVL对需要进行验证的神经网络(包括DNN、CNN、RNN等)系统进行建模,用多维数组表示系统中所涉节点和边的信息,在建模中,用函数表示神经网路系统中的基本操作;确定需要验证的神经网络系统的共有性质特征,主要包括正确性和健壮性,并采用PPTL公式描述神经网络系统的这些性质;将建模的MSVL程序和描述共有性质的PPTL公式统一在UMC4MSVL平台中验证,根据验证结果判断性质是否能够得到满足。本发明将形式化的程序设计过程应用于神经网络系统的建模和验证,程序执行的每一个状态均能够得到可靠的验证,有效地保障了系统本身的安全性。