VDM 中的国际量制库
软件工程
2023-11-17 v1
摘要
国际量制（ISQ）标准发布于 1960 年，以驯服全球范围内发展起来的五花八门的测量系统，例如厘米-克-秒制与米-千克-秒制。该标准深受在不兼容单位间转换时“微不足道”（却易出错）的错误的潜在可能所推动。空间任务、医疗设备等领域曾发生此类事故，致使建模或仿真实验不可用或不安全。我们通过提供一个 \textbf{SAFE}-ISQ VDM 库来解决此问题，该库具备：简单（Simple）、准确（Accurate）、快速（Fast）与有效（Effective）的特点。它扩展了其他 VDM 数学工具包扩展的生态系统，其中包括位于 https://github.com/leouk/VDM_Toolkit 的 VDM 在 Isabelle 中的翻译与证明环境。
引用
@article{arxiv.2311.09704,
title = {International System of Quantities library in VDM},
author = {Leo Freitas},
journal= {arXiv preprint arXiv:2311.09704},
year = {2023}
}
备注
14 pages,, 1 figure, 21st Overture Workshop, Lubeck 2023