Malfunctions in software like airplane control systems or nuclear plant control systems can have catastrophic consequences. Formal verification is the only form of sofware testing that can guarantee the absence of bugs. Formally verified software gives a mathematical proof that the specification is correctly implemented and that no bugs would induce unwanted behaviour. This has a high development cost and having an entirely verified program takes time and effort. However, having verified components already has great benefits. We implement in Scala and formally verify with Stainless a hash map that can then be reused and act as a basis on which to rely. The implementation we propose is based on the LongMap of the Scala standard library with some minor adaptations. This map is implemented with mutable arrays. We give the specification with respect to an implementation of a map based on a list of tuples, that we implement and formally verify as well.
翻译：象飞机控制系统或核电站控制系统这样的软件的功能失灵可能产生灾难性后果。 正式核查是能够保证没有错误的唯一软体测试形式。 正式核查的软件提供了一个数学证据, 证明规格得到正确执行, 没有错误会引起不想要的行为。 开发成本高, 程序经过完全核查需要时间和精力。 但是, 已经核实的部件已经有很大的好处 。 我们在Scala 执行一张可以再利用的散列地图, 并与Stainless 一起正式核查, 并以此为依据。 我们提议的执行以Scala 标准库长映射为基础, 并进行一些小的修改 。 该地图是用变形阵列执行的。 我们给出执行地图的规格, 以图具清单为基础, 我们执行并正式核实地图 。
相关内容
微信扫码咨询专知VIP会员