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).

翻译：信息物理系统与机器人系统的形式化验证要求我们能够精确建模现实世界中存在的物理量。在这些物理量中使用显式单位可以提高严谨性，因为我们可以确保计算中量的兼容性。同时，单位使用不当可能成为安全障碍，因此对物理计算进行自动化合理性检查极具价值。本文在Isabelle/HOL中贡献了国际量值系统（ISQ）及关联的SI单位系统的机械化实现。我们展示了如何利用Isabelle为物理量提供类型系统及自动化证明支持。量值通过维度类型参数化——这些维度类型对应基向量，因此只有相同维度的量值才能相等。由于底层的"量值代数"在量值和SI类型上诱导出同余关系，我们开发了专门的策略支持来捕捉这些关系。我们的构造通过一组已知的量值与SI单位等价性测试集进行了验证。此外，所提出的理论还可用于在SI系统与其他系统（如英制单位系统BIS）之间进行类型安全的转换。