## Runtime Verification of Information Security Policies

Analysis of complex security and privacy policies such as information involves reasoning about multiple execution traces. This stems from the fact that an external observer may gain knowledge about the system through observing and comparing several executions. Monitoring of such policies is highly challenging because most existing monitoring techniques are limited to the analysis of a single trace at run time. In this research project, we are developing an efficient framework for the runtime verification of information security polices for both sequential and concurrent systems. Our long term goal is to implement developed algorithms into mobile devices (e.g., Android), social media platforms (e.g., Facebook) and critical web-based applications (banking institutions web-sites).

## Peroformance Analysis of (Optical) Communication Networks

Network dependability reflects the ability to deliver continuous services even after failures, such as man-made or natural disturbances, e.g., storms, hurricanes, and floods, etc. In this research project, we aim at formal specification of fault tolerant optical networks such as double-rings with dual attachments (DRDA) topologies. Initially, we have utilized the formalism of Continuous-Time Markov Chains (CTMCs) and Continuous Stochastic Logic (CSL) for the prediction of performance metrics for generic optical communication network. In our ongoing work, we are looking at the parameter synthesis for such complex networks, which can provide critical information at early design stages to network operators for designing highly-dependable optical networks in metropolitan areas (e.g., availability on the order of 99.99% or 99.999%).

## Formal Verification of Optical Systems

Optical systems are becoming increasingly important by resolving many bottlenecks in todays communication, electronics, and biomedical systems. However, given the continuous nature of optics, the inability to efficiently analyze optical system models using traditional paper-and-pencil and computer simulation approaches sets limits especially in safety-critical applications. In this research project, we propose a higher-order logic formalization of geometrical optics which includes optical imaging, optical resonators and Gaussian beams. Our formalization is mainly based on theories of multivariate analysis in the HOL Light theorem prover. In order to demonstrate the effectiveness of our proposed approach, we conduct the formal analysis of some real-world optical systems, e.g., an ophthalmic device for eye, a Fabry-Perot resonator, an optical phase-conjugated ring resonator and a receiver module of the APEX telescope.

More Details## Formal Anlysis of Signal Processing Systems in HOL

Signal processing is an emerging area of research which provides the basis to build high-speed communcation systems. Recent advancements in the fabrication technology allow on-chip manufacturing of such signal processing devices. This poses an additional challenge of accurate modeling and analysis due to the complex nature of light and optical components. In this researhc project, we propose to use higher-order-logic theorem proving to improve the analysis accuracy by overcoming the known limitations of incompleteness and soundness of existing approaches (e.g., paper-and-pencil based proofs and simulation). Our main focus is both electronic and photonic signal processing systems.

More Details## Formalization of Fractional Calculus in Higher-Order Logic

Fractional calculus is a generalization of classical theories of integration and differentiation to arbitrary order (i.e., real or complex numbers). In the last two decades, this new paradigm has been widely used to model and analyze a wide class of physical systems in various fields of science and engineering. In this project, we plan to formalize the basic theory of fractional calculus in higher-order-logic. In particular, we require the the corresponding formalization of the Gamma function, Laplace transform, Z-transform and R-transform along with their important properties such as linearity and uniqueness, etc. In this project, we are using HOL Light theorem prover due to the availability of rich multivariate analysis libraries and some closely related projects about optics and signal processing. Our long term goal is to build the reasoning support which ultimately enable us to formally analysis wide class of fractional order systems, e.g., fractional order control, electromagnetics, signal processing and electrical networks.

More Details