一种自动验证的起落架系统原型
软件工程
2022-01-03 v1 计算机科学中的逻辑
摘要
在本文中，我们展示基于集合论的约束逻辑程序设计（CLP）语言 （读作“setlog”）如何被用作 B 规约的自动化验证器。具体而言，我们将 Mammar 与 Laleau 所开发的、被称为起落架系统（LGS）案例研究的 Event-B 规约编码进 中。接下来我们使用 来解除 Rodin 平台在该 Event-B 规约中提出的全部证明义务。以此方式，该 程序可被视为 LGS 的一个自动验证原型。我们相信此案例研究为 CLP 与集合论如何协同作为程序验证的工具提供了经验证据。
引用
@article{arxiv.2112.15147,
title = {An Automatically Verified Prototype of a Landing Gear System},
author = {Maximiliano Cristiá and Gianfranco Rossi},
journal= {arXiv preprint arXiv:2112.15147},
year = {2022}
}