摘要
本发明属于软件工程的规范挖掘技术,为一种近似规范挖掘模型的构建方法及软件行为验证系统。其构建方法包括:根据正例集合,生成一组用于刻画正例时序属性的线性时态逻辑LTL公式;使用LTL公式,生成用于评估及用于训练的潜在负例;设计并构建神经网络,用于从参数赋值中解析出有限状态自动机,以模拟有限状态自动机的接受行为;通过梯度下降算法迭代搜索神经网络,直至达到最大迭代次数,挖掘得到有限状态自动机。本发明的神经网络在推理过程能够模拟有限状态自动机接受,且可低成本地解释出有限状态自动机,解决了搜索空间爆炸问题。