TLA+形式化验证在软件设计中的研究和应用

• 作者: 姜振宇
• 来源期刊: 科学大众
• 学科: 工学
• 关键词: 软件设计 正确性 TLA+形式化验证
• 年，卷（期）: kxdz_2021,（1）
• 页码范围: 79-81
• 页数: 3页
• 分类号: TP3

摘要

为了保证软件产品的正确性,常会采用领域驱动设计、代码重构、测试分层和自动化测试等各种方法。如果在软件设计阶段出现错误,往往要到测试阶段才能发现,尤其在分布式并发环境下,有些错误很微妙,测试阶段难以发现,发现后也难以复现和定位。然而,如何验证软件设计的正确性是现阶段软件行业面临的一个难点问题。近年来,经过亚马逊、微软等公司的探索和实践,TLA+形式化验证技术很好地解决了这个难题。通过使用TLA+对设计方案进行建模并验证模型的正确性,能在软件开发的早期阶段发现并消除难以被测试出来的设计上的错误。