Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL

TL;DR

This paper presents a formalization of physical quantities and SI units in Isabelle/HOL, enabling automated verification of unit correctness and conversions in cyber-physical systems.

Contribution

It introduces a mechanization of the ISQ and SI units in Isabelle/HOL, including a type system for physical quantities and automated proof support for unit consistency.

Findings

Validated by a test set of known equivalences.

Supports type-safe conversions between SI and other systems.

Provides a framework for automated sanity checking of physical calculations.

Abstract

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