Performance Analysis of Systems and Software using a Theorem Prover [ PDF ]
Organizer and Presenter: Osman Hasan and Sofi`ene Tahar, Concordia University, Canada
Abstract: Nowadays, computer simulation is one of the most widely used performance analysis technique. However, simulation based analysis usually provides approximate results due to its inherent nature and it cannot handle large-scale problems due to its enormous CPU time requirements. The unreliability of the results poses a serious problem in safety critical applications, such as those in space travel, military, and medicine, where a mismatch between the predicted and the actual system performance may result in either inefficient usage of the available resources or by unnecessarily paying higher costs to meet some performance or reliability criteria. A possible solution for overcoming these limitations is to conduct performance analysis within the environment of a higher-order-logic theorem prover. Higher-order-logic is a system of deduction with a precise semantics and can be used for the development of almost all classical mathematical theories. Whereas, interactive theorem proving is the field of computer science and mathematical logic concerned with computer based formal proof tools that require some sort of human assistance. Due to the high expressiveness of the higher-order-logic and the inherent soundness of interactive theorem proving, this approach can be used to conduct error free performance analysis at the cost of significant user interaction.
There has been some fruitful developments in this emerging area and a preliminary infrastructure has been proposed that allows the formalization of random variables in higherorder-logic and the formal verification their useful probabilistic and statistical properties within the theorem prover. The main focus of the tutorial is to introduce this new area of research and present its practical effectiveness for conducting precise performance analysis of real world system and software examples.
The tutorial begins by presenting a comprehensive introduction to formal methods and their usefulness in the system design process. It is followed by an overview of the HOL theorem prover, which is the higher-order-logic theorem prover that we have used in this project. Next, we present the process of formalizing (or modeling) random variables and verifying their correctness by proving the corresponding probabilistic and statistical properties, such as mean and variance, in HOL. These formalized random variables can be used to model the uncertainties and random elements found in a system and thus allow us to reason about its performance issues in HOL. For illustration purposes, we present the performance analysis of two examples. Firstly, we verify the average number of trials required for the Coupon Collector’s problem, which is a well known commercially used algorithm. Next, we verify the average delay relations for three commonly used Automated Repeat Request (ARQ) protocols, i.e., Stop-and-Wait, Go-Back-N and Selective-Repeat using the HOL theorem
prover.
This website is maintained by the ISPASS-2008 Committee.
Contact Byeong Kil Lee if you have any questions.