Formal verification of cyber-physical and robotic systems requires that we can accurately model physical quantities that exist in the real-world. The use of explicit units in such quantities can allow a higher degree of rigour, since we can ensure compatibility of quantities in calculations. At the same time, improper use of units can be a barrier to safety and therefore it is highly desirable to have automated sanity checking in physical calculations. In this paper, we contribute a mechanisation of the International System of Quantities (ISQ) and the associated SI unit system in Isabelle/HOL. We show how Isabelle can be used to provide a type system for physical quantities, and automated proof support. Quantities are parameterised by dimension types, which correspond to base vectors, and thus only quantities of the same dimension can be equated. Since the underlying "algebra of quantities" induces congruences on quantity and SI types, specific tactic support is developed to capture these. Our construction is validated by a test-set of known equivalences between both quantities and SI units. Moreover, the presented theory can be used for type-safe conversions between the SI system and others, like the British Imperial System (BIS).
翻译:对网络物理和机器人系统的正式核查要求我们能够准确地模拟现实世界中存在的物理数量。使用这种数量的清晰单位可以更加严格,因为我们可以在计算中确保数量的一致性。与此同时,不适当地使用单位可能会成为安全的障碍,因此,在物理计算中进行自动理智检查是十分可取的。在本文件中,我们促进国际数量系统(ISQ)和伊莎贝尔/HOL中相关的SI单元系统的机械化。我们展示了如何利用伊莎贝尔提供物理数量和自动验证支持的型号系统。数量按与基矢量相对应的尺寸类型进行参数化,因此只能将同一尺寸的数量等同起来。由于基本的“数量代数”在数量和SI类型上引起一致性,因此开发了具体的战术支持来捕捉这些内容。我们的结构通过数量和SI单位之间已知的等同性测试设置得到验证。此外,提出的理论可以用于SIIS系统和其他单位之间的类型安全转换(如英国帝国系统)。