近年来,机器学习系统在社会各领域都有着广泛的应用。然而,由于其安全性和可靠性无法保证,在一些应用中可能造成重大的灾难,尤其在安全攸关系统中,一旦发生错误,其后果是无法接受的。形式化验证方法可以从数学的角度描述算法模型与期望性质,从而提高机器学习系统的安全性,不过系统的底层算法,如泰勒展开等,缺乏深入的形式化研究工作。命题投影时序逻辑PPTL（Propositional Projection Temporal Logic）是一种形式化性质描述逻辑,包含的索引表达式可以等价的表示线性时序逻辑LTL（Linear Temporal Logic）的strong until和weak until操作符。本文使用含索引表达式的PPTL定义泰勒展开过程,使用建模、仿真与验证语言MSVL（Modeling,Simulation and Verification Language）实现了索引表达式描述的泰勒展开,通过模型检测对期望性质进行验证。本文对泰勒展开的两个应用领域近似计算与梯度下降分别进行模型建立、性质提取与验证分析。首先,使用PPTL和索引表达式定义的strong until操作符形式化定义近似计算与梯度下降的过程。然后,实现MSVL中的高精度计算方法,并应用到近似计算与梯度下降模型。最后,使用PPTL公式刻画两种模型的性质,将MSVL程序与PPTL公式输入到统一模型检测器UMC4M中完成性质的验证。在近似计算中,使用MSVL对sin x,cos x,ex三种初等函数的泰勒展开进行建模;针对泰勒展开的结果,使用两种不同的展开结束条件进行计算,将计算结果与可信计算软件ISReal、C中相关函数以及Java中Big Decimal的计算结果进行对比,定义并验证了计算准确性;针对泰勒展开的余项,定义并验证了收敛正确性;针对泰勒展开的项数,对激活函数sigmoid进行计算,定义并验证了快速收敛性。在梯度下降中,首先对迈阿密房价数据集进行预处理,其次用MSVL构建多元线性回归模型,包括预测算法与训练算法;然后对模型进行训练,从特征权值和预测值的相关性角度出发,研究其与训练轮次的关系,定义并验证了相关可变性;为了研究迭代过程中特征权值变化与同一样本的关系,定义并验证了样本影响不变性。