ISSN 1009-5624 CN 10-2021/TQ 主管:中国乐凯集团有限公司 主办:北京乐凯科技有限公司
中国知网全文收录期刊
万方数据库收录期刊
RCCSE中文学术期刊
维普资讯网/超星域出版 全文收录
中国核心期刊(遴选)数据库收录期刊
万方数据库收录期刊
RCCSE中文学术期刊
维普资讯网/超星域出版 全文收录
中国核心期刊(遴选)数据库收录期刊
ISSN 1009-5624 CN 10-2021/TQ 主管:中国乐凯集团有限公司 主办:北京乐凯科技有限公司
【摘要】形式化验证通过数学方法穷尽系统模型的状态空间，能够有效发现软硬件系统的潜在错误。 针对数据库管理系统（ＤＢＭＳ）在人工智能时代面临的复杂性和安全性挑战，本文探讨了形式化验证方法的作用。 通过分析基于 Ｃｏｑ 定理证明器和 ＴＬＡ＋形式化规范语言的验证案例，研究了形式化验证在 ＤＢＭＳ 设计、开发和测试中的应用过程。 结果表明：形式化验证能够有效发现潜在错误，提高 ＤＢＭＳ 的可靠性和安全性，为数据库系统开发提供严谨的理论支撑，具有重要的实际价值。
