基于形式化验证的软件开发模型的验证方法

摘要

本发明提供了一种基于形式化验证的软件开发模型的验证方法，将形式化验证与软件开发过程结合起来，提高软件的高可信程度，从逻辑上保障开发软件的可靠性；发挥形式化验证在软件检错领域的对于软件开发过程中开发逻辑进行验证的作用；降低程序在非正常状态运行的可能性。本发明提高软件的高可信程度，从逻辑上保障开发软件的可靠性；在需求阶段进行验证，可以避免因为软件需求分析不合理导致重新开发的严重后果；及时发挥形式化验证在软件检错领域的对于软件开发过程中函数逻辑正确性进行验证的作用；将形式化方法引入软件开发过程，并给出具体的模型，解决了测试技术在软件检错领域的局限性问题。