Email Gateway (Aug 18 2022 at 11:38): Email Gateway (Aug 18 2022 at 11:38):From: Osman Hasan <o_hasan@ece.concordia.ca>
We apologize if you receive multiple copies of this email.
======================================================================
Half Day Tutorial on
"Performance Analysis of Systems and Software using a Theorem Prover"
2008 IEEE International Symposium on Performance Analysis of Systems and
Software
(ISPASS` 2008)
April 20, 2008
Austin, Texas
CALL FOR PARTICIPATION
======================================================================
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 Collectors problem, which is a well known commercially used
algorithm. Next, we verify the average message delay relation for the
Stop-and-Wait protocol, which is a commonly used Automated Repeat Request
(ARQ) protocol.
Organizers
Osman Hasan and Sofiene Tahar,
{o_hasan,tahar@ece.concordia.ca}
Concordia University,
Montreal, Canada
Important Dates
Early Registeration until: April 4th, 2008
Tutorial Date: April 20th, 2008
More Information
For registeration and more details
http://ispass.org/ispass2008/
Last updated: May 03 2024 at 08:18 UTC