Share Email Print

Proceedings Paper

Formal analysis of electromagnetic optics
Author(s): Sanaz Khan-Afshar; Osman Hasan; Sofiène Tahar
Format Member Price Non-Member Price
PDF $17.00 $21.00

Paper Abstract

Optical systems are increasingly being used in safety-critical applications. Due to the complexity and sensitivity of optical systems, their verification raises many challenges for engineers. Traditionally, the analysis of such systems has been carried out by paper-and-pencil based proofs and numerical computations. However, these techniques cannot provide accurate results due to the risk of human error and inherent approximations of numerical algorithms. In order to overcome these limitations, we propose to use theorem proving (i.e., a computer-based technique that allows to express mathematical expressions and reason about their correctness by taking into account all the details of mathematical reasoning) as a complementary approach to improve optical system analysis. This paper provides a higher-order logic (a language used to express mathematical theories) formalization of electromagnetic optics in the HOL Light theorem prover. In order to demonstrate the practical effectiveness of our approach, we present the analysis of resonant cavity enhanced photonic devices.

Paper Details

Date Published: 12 September 2014
PDF: 14 pages
Proc. SPIE 9193, Novel Optical Systems Design and Optimization XVII, 91930A (12 September 2014); doi: 10.1117/12.2062965
Show Author Affiliations
Sanaz Khan-Afshar, Concordia Univ. (Canada)
Osman Hasan, Concordia Univ. (Canada)
Sofiène Tahar, Concordia Univ. (Canada)

Published in SPIE Proceedings Vol. 9193:
Novel Optical Systems Design and Optimization XVII
G. Groot Gregory; Arthur J. Davis, Editor(s)

© SPIE. Terms of Use
Back to Top
Sign in to read the full article
Create a free SPIE account to get access to
premium articles and original research
Forgot your username?