Formal Analysis of Ray Optics Models in HOL
Ray and wave optics, in which light is characterized as rays and scalar waves,
respectively, provide an efficient and scalable formalism for the modelling
and analysis of optical and laser systems. The main applications are stability analysis of optical resonators, laser mode-locking, polarization
devices and optical reversible circuits. We plan to formalize two well-known theories:
ray-transfer matrices for ray optics and Muller's matrix calculus for wave optics.
Building on these theories, we will be able to reason about different practical aspects
of optical and laser systems such as stability, beam and polarization analysis as
outlined in the following figure.
We have formalized some fundamentals of ray optics and also applied our work to formally analyze the stability of some practical optical resonators. You can find the HOL script in the following line:
[1] U. Siddique and S. Tahar: Towards the Formal Analysis of Microresonators Based Photonic Systems, IEEE/ACM Design Automation & Test in Europe (DATE), 2014 (To Appear).
[2] U. Siddique, V. Aravantinos, and S. Tahar: A New Approach for the Verification of Optical Systems [In: J. Sasin and R.N. Youngworth (Eds.), Optical System Alignment, Tolerancing, and Verification VII (SPIE'13), Proc. SPIE 8844, 2013, pp. 88440G1-88440G-14]
[3] U. Siddique, V. Aravantinos, and S. Tahar: On the Formal Analysis of Geometrical Optics in HOL [In: T. Ida and J. Fleuriot (Eds.), Automated Deduction in Geometry, Lecture Notes in Computer Science 7993, Springer Verlag, 2013, pp. 161-180.]
[4] U. Siddique, V. Aravantinos, and S. Tahar: Formal Stability Analysis of Optical Resonators [In: G. Brat, N. Rungta, and A. Venet (Eds.), NASA Formal Methods Symposium (NFM'13), Lecture Notes in Computer Science 7871, Springer Verlag, 2013, pp. 368-382.]
[5] U. Siddique, V. Aravantinos and S. Tahar: Higher-Order Logic Formalization of Geometrical Optics [In: T. Ida and J. Fleuriot (Eds.), Automated Deduction in Geometry (ADG'12), Informatics Research Report, School of Informatics, University of Edinburgh, Edinburgh, UK, September 2012, pp. 184-196.]
HOL Code Scripts
References
[1] U. Siddique and S. Tahar: Towards the Formal Analysis of Microresonators Based Photonic Systems, IEEE/ACM Design Automation & Test in Europe (DATE), 2014 (To Appear).
[2] U. Siddique, V. Aravantinos, and S. Tahar: A New Approach for the Verification of Optical Systems [In: J. Sasin and R.N. Youngworth (Eds.), Optical System Alignment, Tolerancing, and Verification VII (SPIE'13), Proc. SPIE 8844, 2013, pp. 88440G1-88440G-14]
[3] U. Siddique, V. Aravantinos, and S. Tahar: On the Formal Analysis of Geometrical Optics in HOL [In: T. Ida and J. Fleuriot (Eds.), Automated Deduction in Geometry, Lecture Notes in Computer Science 7993, Springer Verlag, 2013, pp. 161-180.]
[4] U. Siddique, V. Aravantinos, and S. Tahar: Formal Stability Analysis of Optical Resonators [In: G. Brat, N. Rungta, and A. Venet (Eds.), NASA Formal Methods Symposium (NFM'13), Lecture Notes in Computer Science 7871, Springer Verlag, 2013, pp. 368-382.]
[5] U. Siddique, V. Aravantinos and S. Tahar: Higher-Order Logic Formalization of Geometrical Optics [In: T. Ida and J. Fleuriot (Eds.), Automated Deduction in Geometry (ADG'12), Informatics Research Report, School of Informatics, University of Edinburgh, Edinburgh, UK, September 2012, pp. 184-196.]
