Improved bound for stochastic formal correctness of numerical algorithms

Autor: David Lester, Marc Daumas, Érik Martin-Dorel, Annick Truffert
Rok vydání: 2010
Předmět:
Zdroj: Innovations in Systems and Software Engineering. 6:173-179
ISSN: 1614-5054
1614-5046
Popis: We provide bounds on the probability that accumulated errors were never above a given threshold on numerical algorithms. Such algorithms are used, for example, in aircraft and nuclear power plants. This report contains simple formulas based on Levy's, Markov's and Hoeffding's inequalities and it presents a formal theory of random variables with a special focus on producing concrete results. We select three very common applications that cover the common practices of systems that evolve for a long time. We compute the number of bits that remain continuously significant in the first two applications with a probability of failure around one out of a billion, where worst case analysis considers that no significant bit remains. We are using PVS as such formal tools force explicit statement of all hypotheses and prevent incorrect uses of theorems.
Databáze: OpenAIRE
Externí odkaz: