An optical resonator usually consists of mirrors or lenses which are configured in such a way that the beam of light is confined in a closed path. Resonators are fundamental components used in many safety-critical optical and laser applications such as laser surgery, aerospace industry and nuclear reactors. Due to the complexity and sensitivity of optical resonators, their verification poses many challenges to optical engineers. Traditionally, the stability analysis of such resonators, which is the most critical design requirement, has been carried out by paper-and-pencil based proof methods and numerical computations. However, these techniques cannot provide accurate results due to the risk of human error and the inherent incompleteness of numerical algorithms. In this paper, we propose to use higher-order logic theorem proving for the stability analysis of optical resonators. Based on the multivariate analysis library of HOL Light, we formalize the notion of light ray and optical system (by defining medium interfaces, mirrors, lenses, etc.). This allows us to derive general theorems about the behaviour of light in such optical systems. In order to illustrate the practical effectiveness of our work, we present the formal analysis of a Fabry-Pérot resonator with fiber rod lens.
展开▼
