Formal modeling and verification of integrated photonic systems

The prominent advantages of photonics are high bandwidth, low power and the possibility of better electromagnetic interference immunity. As a result, photonics technology is increasingly used in ubiquitous applications such as telecommunication, medicine, avionics and robotics. One of the main critical requirements is to verify the corresponding functional properties of these systems. In this perspective, we identify the most widely used modeling techniques (e.g., transfer matrices, difference equations and block diagrams) for the modeling and analysis of photonic components. Considering the safety and cost critical nature of the application domain, we discuss the potential of using formal methods as a complementary analysis approach. In particular, we propose a framework to formally specify and verify the critical properties of complex photonic systems within the sound core of a higher-order-logic theorem prover. For illustration purposes, we present the formal specification of a microring resonator based photonic filter along with the verification of some important design properties such as spectral power and filtering rejection ratio.