Current Projects:
Active Projects
Completed Projects
Description
Paper and pencil analysis and computer simulations have traditionally been used in reliability analysis of engineering systems. Formal methods based techniques provide an accurate and complementary alternative to these techniques. In this research, we have developed a formal reliability analysis approach based on higher-order logic theorem proving. The formal reliability analysis method is shown in the Figure above. Our proposed approach facilitates verification, computation, reasoning, and documentation of the reliability proofs in the sound environment of the HOL theorem prover. The green boxes below the top dotted line highlight some of the main features of the proposed reliability analysis method. The higher-order logic theories we have developed enable lifetime reliability modeling using single and multiple random variables. We can prove reliability properties of various engineering system configurations such as series, parallel, series-parallel and parallel-series structures. We have applied the developed theories to the problems in fault modeling, and reliability analysis of electronic systems. Following are selected peer reviewed publications that highlight our work.
Active Projects
- Formal Probabilistic Risk Assessment using Theorem Proving
- Formal Dynamic Dependability Analysis using HOL Theorem Proving
Completed Projects
Description
Approximate Computing (AC) or inexact computing is a computation technique resulting in inaccurate results in favor of power, area and delay savings. AC can be applied in error tolerant applications, e.g., search engines and multimedia processing. AC is gaining traction as a computing paradigm since transistor's scaling has seen its lowest pace in the past few years, and a breakthrough is indispensable in order to make computers faster in the future.
