Grant: Discovery Grants Program - Individual

Physical systems and devices are increasingly being used in safety-critical domains, such as electronic medicine equipment and automated transportation. The verification of such systems has predominantly been accomplished by analytical techniques or simulation testing. However, as engineering systems are getting more complex the confidence level in such traditional verification techniques is rapidly decreasing. These limitations can, however, be overcome by using formal methods for the modeling and validation of physical systems through deductive reasoning. In this research program, we aim in particular at using higher-order logic based theorem proving to formally analyze and verify physical systems. Higher-order logic is a system of deduction with a precise semantics and is expressive enough to be used for the specification of almost all classical mathematics theories. Theorem proving is the field of computer science and mathematical logic concerned with precise computer based formal proof tools that require some sort of human assistance. In the proposed research, we are interested in analyzing the probabilistic and statistical behavior of systems by formalizing in higher-order logic queuing and information theory fundamentals. Immediate applications include the analysis of telecommunications systems performance, roundoff errors of arithmetic computing or error coding in digital media. We also plan to formalize specific mathematical theories widely used in the target domains of optics and aeronautics to be able to reason about properties of optical interconnects and flight control stability, respectively. Finally, we aim at investigation prospects of using numerical analysis with automated theorem proving for checking the reliability of nanoelectronics circuits. We believe that our approaches will advance the state-of-the-art in systems specification and verification, thus significantly enhancing the confidence level in the correctness of safety critical products. The direct beneficiary of this research will be the Canadian telecommunications, optics, microelectronics and aeronautics industry. Furthermore, this proposal will contribute towards the training of a number of skilled personnel available to Canadian industry and academia.