1: %
2: %
3: %
4: %
5: %
6: %
7: %
8: %
9: %
10: %
11: %
12: %
13: %
14: %
15: %
16: %
17: %
18: %
19: %
20: %
21: %
22:
23: %
24: %
25: %
26: %
27: %
28: %
29:
30:
31: %
32: %
33: %
34: %
35: %
36: %
37: %
38: %
39: %
40: %
41: %
42: %
43: \documentclass[conference]{IEEEtran}
44: %
45: %
46: %
47:
48:
49: %
50:
51: \usepackage{cite} % Written by Donald Arseneau
52: % V1.6 and later of IEEEtran pre-defines the format
53: % of the cite.sty package \cite{} output to follow
54: % that of IEEE. Loading the cite package will
55: % result in citation numbers being automatically
56: % sorted and properly "ranged". i.e.,
57: % [1], [9], [2], [7], [5], [6]
58: % (without using cite.sty)
59: % will become:
60: % [1], [2], [5]--[7], [9] (using cite.sty)
61: % cite.sty's \cite will automatically add leading
62: % space, if needed. Use cite.sty's noadjust option
63: % (cite.sty V3.8 and later) if you want to turn this
64: % off. cite.sty is already installed on most LaTeX
65: % systems. The latest version can be obtained at:
66: % http://www.ctan.org/tex-archive/macros/latex/contrib/supported/cite/
67:
68: %
69: % Required if you want graphics, photos, etc.
70: % graphicx.sty is already installed on most LaTeX
71: % systems. The latest version and documentation can
72: % be obtained at:
73: % http://www.ctan.org/tex-archive/macros/latex/required/graphics/
74: % Another good source of documentation is "Using
75: % Imported Graphics in LaTeX2e" by Keith Reckdahl
76: % which can be found as esplatex.ps and epslatex.pdf
77: % at: http://www.ctan.org/tex-archive/info/
78: %
79: %\ifx\pdfoutput\undefined
80: \usepackage{graphicx}
81: %\else
82: %\usepackage[pdftex]{graphicx}
83: %\fi
84:
85: %
86: %
87: %
88: %
89: %
90: %
91: %
92: %
93: %
94: %
95: %
96: %
97: %
98: %
99: %
100: %
101: %
102:
103:
104: %
105: % and David Carlisle
106: % This package allows you to substitute LaTeX
107: % commands for text in imported EPS graphic files.
108: % In this way, LaTeX symbols can be placed into
109: % graphics that have been generated by other
110: % applications. You must use latex->dvips->ps2pdf
111: % workflow (not direct pdf output from pdflatex) if
112: % you wish to use this capability because it works
113: % via some PostScript tricks. Alternatively, the
114: % graphics could be processed as separate files via
115: % psfrag and dvips, then converted to PDF for
116: % inclusion in the main file which uses pdflatex.
117: % Docs are in "The PSfrag System" by Michael C. Grant
118: % and David Carlisle. There is also some information
119: % about using psfrag in "Using Imported Graphics in
120: % LaTeX2e" by Keith Reckdahl which documents the
121: % graphicx package (see above). The psfrag package
122: % and documentation can be obtained at:
123: % http://www.ctan.org/tex-archive/macros/latex/contrib/supported/psfrag/
124:
125: %
126: % This package makes it easy to put subfigures
127: % in your figures. i.e., "figure 1a and 1b"
128: % Docs are in "Using Imported Graphics in LaTeX2e"
129: % by Keith Reckdahl which also documents the graphicx
130: % package (see above). subfigure.sty is already
131: % installed on most LaTeX systems. The latest version
132: % and documentation can be obtained at:
133: % http://www.ctan.org/tex-archive/macros/latex/contrib/supported/subfigure/
134:
135: \usepackage{url} % Written by Donald Arseneau
136: % Provides better support for handling and breaking
137: % URLs. url.sty is already installed on most LaTeX
138: % systems. The latest version can be obtained at:
139: % http://www.ctan.org/tex-archive/macros/latex/contrib/other/misc/
140: % Read the url.sty source comments for usage information.
141:
142: %
143: % Gives LaTeX2e the ability to do double column
144: % floats at the bottom of the page as well as the top.
145: % (e.g., "\begin{figure*}[!b]" is not normally
146: % possible in LaTeX2e). This is an invasive package
147: % which rewrites many portions of the LaTeX2e output
148: % routines. It may not work with other packages that
149: % modify the LaTeX2e output routine and/or with other
150: % versions of LaTeX. The latest version and
151: % documentation can be obtained at:
152: % http://www.ctan.org/tex-archive/macros/latex/contrib/supported/sttools/
153: % Documentation is contained in the stfloats.sty
154: % comments as well as in the presfull.pdf file.
155: % Do not use the stfloats baselinefloat ability as
156: % IEEE does not allow \baselineskip to stretch.
157: % Authors submitting work to the IEEE should note
158: % that IEEE rarely uses double column equations and
159: % that authors should try to avoid such use.
160: % Do not be tempted to use the cuted.sty or
161: % midfloat.sty package (by the same author) as IEEE
162: % does not format its papers in such ways.
163:
164: \usepackage{amsmath} % From the American Mathematical Society
165: % A popular package that provides many helpful commands
166: % for dealing with mathematics. Note that the AMSmath
167: % package sets \interdisplaylinepenalty to 10000 thus
168: % preventing page breaks from occurring within multiline
169: % equations. Use:
170: \interdisplaylinepenalty=2500
171: % after loading amsmath to restore such page breaks
172: % as IEEEtran.cls normally does. amsmath.sty is already
173: % installed on most LaTeX systems. The latest version
174: % and documentation can be obtained at:
175: % http://www.ctan.org/tex-archive/macros/latex/required/amslatex/math/
176:
177: %
178:
179: %
180: %
181: %
182: %
183: %
184: %
185:
186: %
187: %
188: %
189: %
190: %
191:
192:
193: %
194: %
195:
196:
197: %
198:
199: %
200: %
201: %
202:
203:
204:
205: %
206: %
207: %
208: %
209: %
210: %
211: %
212: %
213: %
214: %
215: %
216: %
217: %
218: %
219: %
220: %
221: %
222: %
223: %
224: %
225: %
226: %
227: %
228: %
229: %
230: %
231: %
232: \makeatletter
233: \let\NAT@parse\undefined
234: \makeatother
235: %
236: %
237: %
238: %
239: %\ifx\pdfoutput\undefined
240: \usepackage[hypertex]{hyperref}
241: %\else
242: %\usepackage[pdftex,hypertexnames=false]{hyperref}
243: %\fi
244: %
245: %
246: %
247:
248:
249:
250: %
251: %
252: %
253:
254:
255: %
256: \hyphenation{op-tical net-works semi-conduc-tor IEEEtran}
257:
258: \newtheorem{theorem}{Theorem}
259: \newtheorem{lemma}{Lemma}
260: \newtheorem{definition}{Definition}
261: \newcommand{\ulp}{\text{ulp}}
262: \usepackage[latin9]{inputenc} \usepackage[T1]{fontenc}
263: \usepackage{amsfonts}\newcommand{\R}{\mathbb{R}}\renewcommand{\Pr}{\mathbb{P}}\def\Ex{\mathbb{E}}
264: \usepackage{amssymb}
265: \usepackage{listings}
266: \lstset{numbers=left,
267: numberstyle=\tiny,
268: stepnumber=1,
269: numbersep=5pt,
270: extendedchars=true,
271: basicstyle=\footnotesize,
272: breaklines,
273: showstringspaces=false,
274: frame=lines,
275: xleftmargin=12pt,
276: xrightmargin=6pt,
277: framesep=12pt,
278: language={C},
279: firstnumber=last,
280: mathescape=true
281: }
282:
283: \begin{document}
284:
285: %
286: \title{Stochastic Formal Methods: \\ An application to accuracy of numeric software}
287:
288:
289: %
290: %
291: %
292: \author{\authorblockN{Marc Daumas}
293: \authorblockA{%
294: CNRS-LIRMM visiting LP2A\\
295: University of Perpignan Via Domitia\\
296: Perpignan, France 66860\\
297: Email: Marc.Daumas@Univ-Perp.Fr}
298: \and
299: \authorblockN{David Lester}
300: \authorblockA{%
301: School of Computer Science\\
302: University of Manchester\\
303: Manchester, United Kingdom M13 9PL\\
304: Email: David.R.Lester@Manchester.Ac.UK}
305: }
306:
307: %
308: %
309:
310:
311: %
312: %
313: %
314: %
315: %
316: %
317: %
318: %
319: %
320: %
321: %
322: %
323: %
324: %
325: %
326: %
327:
328:
329:
330: %
331: %
332:
333: %
334: \maketitle
335:
336: %
337: %
338:
339: \begin{abstract}
340: This paper provides a bound on the number of numeric operations
341: (fixed or floating point) that can safely be performed before
342: accuracy is lost. This work has important implications for control
343: systems with safety-critical software, as these systems are now
344: running fast enough and long enough for their errors to impact on
345: their functionality. Furthermore, worst-case analysis would blindly
346: advise the replacement of existing systems that have been
347: successfully running for years. We present here a set of formal
348: theorems validated by the PVS proof assistant. These theorems will
349: allow code analyzing tools to produce formal certificates of
350: accurate behavior. For example, FAA regulations for aircraft
351: require that the probability of an error be below $10^{-9}$ for a 10
352: hour flight \cite{JohBut92}.
353: \end{abstract}
354:
355: %
356:
357: %
358: %
359: %
360: %
361: %
362: %
363: \IEEEpeerreviewmaketitle
364:
365:
366:
367: \section{Introduction}
368: %
369:
370: Formal proof assistants are used in areas where errors can cause
371: loss of life or significant financial damage as well as in areas where common
372: misunderstandings can falsify key assumptions. For this reason, formal
373: proof assistants have been much used in floating point arithmetic
374: \cite{Rus98,Har2Ka,BolDau03,DauMelMun05,MunLes05}. Previous references
375: just link to a few projects using proof assistants such as ACL2, HOL
376: \cite{GorMel93}, Coq \cite{HueKahPau04} and PVS \cite{OwrRusSha92}.
377:
378: All these projects deal with worst case behavior. Recent work has
379: shown that worst case analysis is meaningless for applications that
380: run for a long time. For example, a process adds numbers in $\pm 1$ to
381: single precision, and therefore has a round-off error of $\pm
382: 2^{-25}$. If this process adds $2^{25}$ items, then the accumulated
383: error is $\pm 1$, and note that 10 hours of flight time at operating
384: frequency of 1~kHz is approximately $2^{25}$ operations. Yet we
385: easily agree that provided the round-off errors are not correlated,
386: the actual accumulated error will be much smaller.
387:
388: Developments in probability share many features with developments in
389: floating point arithmetic:
390: \begin{enumerate}
391: \item Each result usually relies on a long list of hypotheses. No
392: hypothesis can be removed, but slight variations induce a large
393: number of results that look almost identical.
394: \item Most people that use the results are not specialists in the
395: specific field. They want a trustworthy result but they are not
396: proficient enough to either select the best scheme or detect minor
397: faults that can quickly lead to huge problems.
398: \end{enumerate}
399:
400: For these reasons, we are strongly of the opinion that validation of a
401: safety-critical numeric software using probability should be done
402: using an automatic proof checker. We present in
403: Section~\ref{sec/stoch} the model that we are using. Section
404: \ref{sec/prob} presents our formal developments in probability. The
405: Doobs-Kolmogorov inequality provides an effective way to compute the
406: probability that a piece of software will successfully run within an
407: acceptable error bound.
408:
409: %
410: %
411: %
412:
413: This work is connected to continuous space Markov random walks or
414: renewal-reward processes though these applications focus on asymptotic
415: behavior \cite{Bre98,Fuh04}. We want to precisely bound the
416: probability of remaining within bounds for a given number of steps.
417: This is connected to ruin probabilities \cite{Asm2K} and the
418: Doobs-Kolmogorov inequality for martingales \cite{GriSti82}. Related
419: work on theoretic construction of the probability space using higher
420: order logic can be found in \cite{Hur02,AudPau06} and references herein. In the
421: rest of this text, we assume that the created round-off and measure
422: errors are unbiased independent random variables or that their
423: expectation conditional to the previous errors is zero.
424:
425: \section{Stochastic model}
426: \label{sec/stoch}
427:
428: \subsection{Individual round-off errors of fixed and floating point
429: operations}
430:
431: We are dealing with fixed or floating point numbers. A floating point
432: number represents $v = m \times 2^e$ where $e$ is an integer and $m$
433: is a fixed point number \cite{Gol91}. IEEE 754 standard \cite{Ste.87}
434: uses sign-magnitude notation for the mantissa and the first bit of the
435: mantissa is implicit in most cases leading to the following definition
436: where $s$ and all the $b_i$ are either 0 or 1 (bits).
437: $$
438: v = (-1)^s \times 1.b_1 \cdots b_{p-1} \times 2^e
439: $$
440: Some circuits such as TMS320 uses two's complement notation for $m$
441: leading to the following definition \cite{Tex97}.
442: $$
443: v = (1.b_1 \cdots b_{p-1} - 2 \times s) \times 2^e
444: $$
445:
446: For both notations, we define for any representable number $x$, the
447: unit in the last place function where $e$ is the exponent of $x$ as
448: above. In fixed point notation, $e$ is a constant provided by the data
449: type.
450: $$
451: \ulp (v) = 2^{e - p + 1}
452: $$
453:
454: A variable $v$ is set either by an external sensor or by an operation.
455: Trailing digits of numbers randomly chosen from a logarithmic
456: distribution \cite[p. 254-264]{Knu97} are approximately uniformly
457: distributed \cite{FelGoo76}. So we can assume that if $v$ is a data
458: obtained by an accurate sensor, the difference between $v$ and the
459: actual value $\overline{v}$ is uniformly distributed in the range $\pm
460: \ulp(v)/2$. We can model the representation error $v - \overline{v}$
461: by a random variable $X$ with expectation $\Ex(X) = 0$ and variance
462: $\Ex(X^2) = \ulp(v)^2/12$. The sensor may be less accurate leading to
463: a larger variance but it should not be biased.
464:
465: Round-off errors created by operators are discrete and they are not
466: necessarily distributed uniformly \cite{BusFelGooLin79}. For each
467: operator $\circledast$ implementing the real operation $\ast$, we
468: define
469: $$X = V \circledast W - V \ast W$$
470: where $V$ and $W$ are number distributed logarithmically over
471: specified ranges. The distribution of $X$ is very specific but we
472: verify that the expectation is $\Ex(X) = 0$ and we bound its variance
473: $\Ex(X^2)$.
474:
475: Fixed point additions do not create any additional round-off error
476: provided its output is in the same format as its inputs. Reducing the
477: format of a fixed point number creates a uniformly distributed round
478: off error provided the input was logarithmically distributed
479: \cite{FelGoo76}.
480:
481: \subsection{Round off errors of an accumulation loop}
482: \label{sub/loop}
483:
484: We will use two examples. The first one is given in
485: listing~\ref{lst/int}. It sums data produced by a fixed point sensor
486: $x_i$ with a measure error $X_i$.
487:
488: \begin{lstlisting}[caption={Simple discrete integration from \cite{BriDauLanMar06}},firstnumber=1,label=lst/int]
489: $a_0 = 0$
490: for ($i = 0$; $i < n$; $i = i + 1$)
491: $a_{i+1} = a_i + x_i$
492: \end{lstlisting}
493:
494: We can safely assume that $X_i$ are independent identical uniformly
495: distributed random variables over $\pm \ulp(x_i)/2$. Data are fixed
496: point meaning that the sum $a_i + x_i$ does not introduce any rounding
497: error and the weigth of one unit in the last place does not depend on
498: $x_i$ so we write $\ulp$ instead of $\ulp(x_i)$. After $n$
499: iterations, we want the probability that the accumulated measure error
500: have always been constrained into user specified bounds $\epsilon$.
501: Using the Doobs-Kolmogorov inequality of Theorem~\ref{theo/doobs}
502: where $S_i = \sum_{j=1}^i X_j$, we have that
503: $$\Pr\left(\max_{1\le i\le n}(|S_i|)\le\epsilon\right) \le 1 - \frac{n \ulp^2}{12 {\epsilon}^2}.$$
504:
505: %
506: %
507:
508: %
509: %
510: %
511: %
512: %
513:
514: The second example is given in listing~\ref{lst/ode}. It solves
515: initial value problem (IVP) ordinary differential equations (ODE) by
516: computing an incremental slope $\Phi(t_i, h_i, x_i, f)$ based on the
517: current time $t_i$, the current step size $h_i$, the current value of
518: the function $x_i$ and the differential equation $x'(t) = f(t, x(t))$.
519: The function $\Phi$ may be very simple using Euler's explicit method
520: or more complex using any Runge-Kutta method or any implicit method.
521: We focus here on scalar ODEs although our analysis may apply to
522: vectors. Line 4 assume for the sake of simplicity that $h_i$ is a
523: constant although this is not neccessary.
524:
525: \begin{lstlisting}[caption={Solving initial value problem ordinary differential equations \cite{StoBur02}},firstnumber=1,label=lst/ode]
526: for ($i = 0$; $i < n$; $i = i + 1$) {
527: $x_{i+1} = x_i + h_i \times \Phi(t_i, x_i, h_i, f)$
528: $t_{i+1} = t_i + h_i$
529: $h_{i+1} = h_i$
530: }
531: \end{lstlisting}
532:
533: Our first guess was to introduce a sequence of random variables
534: $\{X_n\}$ that models the difference introduced by round-off errors at
535: step $i$. In most cases, $\Phi$ introduces a drift due to higher order
536: effect of random variables and a drifted correlation between the error
537: introduced at step $i+1$ and errors on the previous steps. For
538: example, the square of a rounded value $v + V$ where $v$ is the stored
539: value and $V$ is a random variable, introduces a positive drift due to
540: $V^2$ term that is always positive. So we model the effect of the
541: round-off error by two terms $X_i$ and $Y_i$. We use the
542: Doobs-Kolomogorov inequality of Theorem~\ref{theo/doobs} for the
543: sequence $\{X_n\}$ and worst case error analysis for the sequence
544: $\{Y_n\}$ setting the following conditional expectation
545: $$
546: \Ex(X_n; X_1 \cdots X_{n-1}) = 0.
547: $$
548:
549: Random variables $X_{i+1}$ and $Y_{i+1}$ account for the round-off and
550: propagated errors introduced by replacing
551: $$
552: x_i + X_i + Y_i + h_i \times \Phi(t_i, x_i + X_i + Y_i, h_i, f)
553: $$
554: with
555: $$
556: x_i \oplus h_i \otimes \tilde{\Phi}(t_i, x_i, h_i, f)
557: $$
558: where $\tilde{\Phi}$ is evalaution of $\Phi$ in computer. First order
559: effect of round-off errors created are accounted in $X_{i+1}$. Higher
560: order effect of round-off errors created and propagated effect of
561: $X_i$ and $Y_i$ in $\Phi$ are accounted in $Y_{i+1}$.
562:
563: $\{X_n\}$ is constructed to contain only independent random variables with no drift
564: $\Ex(X_i) = 0$ and we only need to bound their variance $\Ex(X_i^2)$.
565: We will do worst case analysis on $\{Y_n\}$ and we bound each $Y_i$
566: with interval arithmetic \cite{JauKieDidWal01}. Software such as
567: Fluctuat \cite{GouMarPut06} is already able to distinguish between first order and higher
568: order error terms.
569:
570: %
571: %
572: %
573: %
574: %
575: %
576: %
577: %
578: %
579: %
580: %
581: %
582:
583: %
584: %
585: %
586: %
587: %
588: %
589: %
590: %
591: %
592: %
593: %
594: %
595: %
596: %
597: %
598: %
599: %
600: %
601:
602: %
603: %
604: %
605: %
606: %
607: %
608: %
609: %
610: %
611: %
612: %
613: %
614: %
615: %
616:
617: %
618: %
619: %
620: %
621: %
622: %
623: %
624: %
625: %
626:
627: %
628: %
629: %
630: %
631: %
632: %
633: %
634: %
635: %
636: %
637: %
638:
639:
640: %
641: %
642: %
643: %
644:
645: \section{Probability distribution of being safe}
646: \label{sec/prob}
647:
648: \subsection{Probability}
649:
650: We have two main choices in presenting an account of probability: one
651: is to take an informal approach, the second involves taking
652: foundational matters seriously. In this paper we will consistently try
653: to present matters informally except for Section~\ref{sub/form},
654: however the reader should be aware that the PVS system underlying
655: these results is built on the firm foundations for probability theory
656: (using measure theory) \cite{Hal44,Hal50}. A middle way between
657: extreme formality and an accessible level of informality is to be
658: found in \cite{GriSti82}.
659:
660: We begin by defining the {\em distribution function} of a random
661: variable.
662: \begin{definition}
663: A random variable $X$ has {\em distribution function} $F$, if
664: $\Pr(X\leq x) = F(x)$
665: \end{definition}
666: As we will be studying {\em continuous random variables}, these are
667: defined as follows:
668: \begin{definition}
669: A random variable $X$ is {\em continuous} if its distribution function
670: can be expressed as
671: \[F(x) = \int_{-\infty}^x f(x) dx\]
672: for some integrable function $f:\R \to [0,\infty)$. We call the
673: function $f$ the probability density function for the random variable
674: $X$.
675: \end{definition}
676: As an example of a continuous random variable, consider the
677: temperature $T$ at a certain point in an industrial process. Even if
678: an attempt is being made to hold this temperature constant, there will
679: be minor fluctuations, and these can be modeled mathematically by
680: assuming that $T$ is a continuous random variable.
681:
682: The other concept we will need is that of dependent and independent
683: random variables. Suppose we model the outcomes of the tossing of two
684: coins $C_1$ and $C_2$ by random variables. Provided there is nothing
685: underhand going on, we would expect the result of tossing the first
686: coin to have no effect on the result of the second coin, and {\it vice
687: versa}. If this is the case, then we say that $C_1$ and $C_2$ are {\em
688: independent}. Consider an alternative scenario in which having tossed
689: the coin $C_1$ and discovered that it has come up ``heads'', and we
690: now define the random variable $C_2$ to be: the outcome: ``the
691: downward facing side of the coin $C_1$ is tails''. In this case the
692: random variables $C_1$ and $C_2$ are {\em dependent}.
693:
694: The other idea we must address is that of {\em conditional probability}.
695: \begin{definition}
696: We define the probability of ``$A$ given $B$'' (written $\Pr(A;~B)$) as:
697: \[\Pr(A;~B) = \frac{\Pr(A\mathrel{\cap}B)}{\Pr(B)}\]
698: whenever $\Pr(B)>0$.
699: \end{definition}
700: As an example: if event $A$ is ``I am carrying an umbrella'' and event
701: $B$ is ``it is raining'', then $Pr(A;~B)$ is the probability that ``I
702: am carrying an umbrella given that it is raining''. Note that although
703: in general $\Pr(A;~B) \not= \Pr(B;~A)$, in this particular case, if
704: you live in Perpignan or Manchester, then on most days: $\Pr(A;~B) =
705: \Pr(B;~A)$, though for rather different reasons.
706:
707: \subsection{A Formal Development of probability}
708: \label{sub/form}
709:
710: \begin{definition}
711: A {\em $\sigma$-algebra} over a type $T$, is a subset of the power-set
712: of $T$, which includes the empty set $\{\}$, and is closed under the
713: operations of complement, countable union and countable intersection.
714: \end{definition}
715:
716: If $T$ is countable -- as it is for discrete random variables -- then
717: we may take $\sigma=\wp(T)$; if the set $T$ is the reals -- as it
718: is for continuous random variables -- then we make $\sigma=B$: the
719: Borel sets.
720:
721: \begin{definition}
722: A {\em Measurable Space} $(T,\sigma)$ is a set (or in PVS a type) T,
723: and a {\em $\sigma$-algebra} over $T$.
724: \end{definition}
725:
726: \begin{definition}
727: A function $\mu:\sigma\to{\R}_{\ge 0}$ is a {\em Measure} over the
728: $\sigma$-algebra $\sigma$, when $\mu(\{\}) = 0$, and for a sequence of disjoint
729: elements $\{E_n\}$ of $\sigma$:
730: \[\mu\left(\bigcup_{n=0}^\infty E_n\right) = \sum_{n=0}^\infty \mu(E_n).\]
731: \end{definition}
732:
733: \begin{definition}
734: A {\em Measure Space} $(T,\sigma,\mu)$ is a measurable space
735: $(T,\sigma)$ equipped with a measure $\mu$.
736: \end{definition}
737:
738: \begin{definition}
739: A {\em Probability Space} $(T,\sigma,\Pr)$ is a measure space
740: $(T,\sigma,\Pr)$ in which the measure $\Pr$ is finite for any set in
741: $\sigma$, and in which:
742: \[\Pr(X^c) = 1-\Pr(X).\]
743: \end{definition}
744:
745: The PVS development of probability spaces in Figure~\ref{lst/prob},
746: takes three parameters: $T$, the sample space, $S$, a $\sigma$-algebra
747: of permitted events, and, $\Pr$, a probability measure, which assigns
748: to each permitted event in $S$, a probability between $0$ and $1$.
749: Properties of probability that are independent of the particular
750: details of $T$, $S$ and $\Pr$ are then provided in this file. If we
751: wished to discuss continuous random variables then we would partially
752: instantiate this PVS file with {\tt T = real}, and {\tt S =
753: borel\_set}. If we go further and also specify $\Pr$, we will have
754: described the random variable distributions as well. Of particular
755: interest later is the fact that the sum of two random variables is
756: itself a random variable, and consequently any finite sum of random
757: variables will be a random variable.
758:
759: \begin{figure*}
760: \begin{center}\fbox{\begin{minipage}{0.98\linewidth}
761: {\footnotesize \input{proba_space}}
762: \end{minipage}}\end{center}
763: \caption{Abbreviated probability space file in PVS}
764: \label{lst/prob}
765: \end{figure*}
766:
767: \begin{definition}
768: If $(T_1,{\sigma}_1,{\Pr}_1)$ and $(T_2,{\sigma}_2,{\Pr}_2)$ are
769: probability spaces then we can construct a {\em product probability
770: space} $(T_3,{\sigma}_3,{\Pr}_3)$, where:
771: \[\begin{array}{lll}
772: T_3 &=& T_1 \times T_2 \\
773: {\sigma}_3 &=& \sigma({\sigma}_1\times {\sigma}_2)\\
774: {\Pr}_3'(a,b) &=& {\Pr}_1(a){\Pr}_2(b)
775: \end{array}\]
776: where ${\Pr}_3$ is the extension of ${\Pr}'_3$ that has the whole of
777: ${\sigma}_3$ as its domain.
778: \end{definition}
779:
780: Note that the product probability ${\Pr}_3$ has the effect of
781: declaring that the experiments carried out in probability spaces
782: $(T_1,{\sigma}_1,{\Pr}_1)$ and $(T_2,{\sigma}_2,{\Pr}_2)$ are
783: independent. Obviously, the process of forming products can be
784: extended to any finite product of finitely many probability
785: spaces. Currently, it is not clear whether PVS is powerful enough to
786: capture the notion of a countably infinite sequence of random
787: variables $\{X_n\}_{n=1}^{\infty}$; fortunately, in this work we don't
788: currently require this result.
789:
790: In Figure~\ref{lst/cond}, we define the conditional probability
791: $\Pr(A;~B)$ (written {\tt P(A,B)} as PVS will not permit the use of
792: ``;'' as an operator). We take the opportunity to prove Bayes' Theorem
793: along the way.
794:
795: \begin{figure*}
796: \begin{center}\fbox{\begin{minipage}{0.98\linewidth}
797: {\footnotesize \input{conditional}}
798: \end{minipage}}\end{center}
799: \caption{Conditional probability file in PVS}
800: \label{lst/cond}
801: \end{figure*}
802:
803: \subsection{Continuous Uniform Random Variables}
804:
805: If $X$ is a continuous random variable distributed uniformly over the
806: interval $[a,b]$, then informally it takes any value within the
807: interval $[a,b]$ with equal probability.
808:
809: To make this more formal, we define the {\em characteristic function}
810: of a set $S$ as the function ${\chi}_S$, which takes the values $1$ or
811: $0$ depending on whether it is applied to a member of $S$.
812: \begin{definition}
813: \[{\chi}_S(x) = \left\{\begin{array}{ll} 1 & x\in S\\
814: 0 & x\not\in S\end{array}\right.\]
815: \end{definition}
816: Now the probability density function $f$ of the uniform random
817: variable over the closed interval $[a,b]$ is
818: $\frac{1}{b-a}{\chi}_{(a,b]}$. From this we can calculate the
819: distribution function:
820: \[F(x) = \int_{-\infty}^x f(x) dx,\]
821: from which we can calculate the probability
822: \[\Pr(x<X<=y) = F(y)-F(x).\]
823:
824: In the case where $X$ is distributed $U_{[0,1]}$, and because -- for
825: any $f(x)$ with $\int f = F$ -- we have
826: $$
827: \begin{array}{l}
828: \displaystyle \int_{-\infty}^\infty f(x) \chi_{(a,b]}(x) dx = \\
829: \displaystyle ~~~~~ (F(x)-F(a))\chi_{(a,b]}(x) + (F(b)-F(a))\chi_{(b,\infty)}(x).
830: \end{array}
831: $$
832:
833: We also observe that if $X$ is distributed $U_{[a,b]}$, then $\Ex(X) =
834: \frac{a+b}{2}$, and $\mbox{Var}(X) = \frac{(a-b)^2}{12}$. So, with
835: $a=0$, $b=1$ we get: $\mu=\frac{1}{2}$, $\sigma^2 = \frac{1}{12}$.
836:
837: %
838:
839: %
840: %
841: %
842: %
843: %
844: %
845: %
846: %
847: %
848:
849: \subsection{Sums of Continuous Random Variables}
850:
851: \begin{definition}
852: If we have a sequence of continuous random variables $\{X_n\}$, then
853: we define their partial sums as a sequence of continuous random
854: variables $\{S_n\}$ with the property
855: \[S_n = \sum_{i=1}^n X_i.\]
856: \end{definition}
857:
858: \begin{theorem}
859: If continuous random variables $X$ and $Y$ have joint probability density
860: functions $f$, then $Z=X+Y$ has probability
861: density function:
862: \[f_Z(z) = \int_{-\infty}^\infty f(x,z-x) dx.\]
863: \end{theorem}
864:
865: In the special case where $X$ and $Y$ are independent, then (because
866: the joint probability density function $f(x,y)$ can be expressed as
867: the product $f_X(x)f_Y(y)$) we have the {\em Continuous Convolution
868: Theorem}:
869: \begin{theorem}
870: If continuous random variables $X$ and $Y$ are independent and have
871: probability density functions $f_X$ and $f_Y$ respectively, then
872: $Z=X+Y$ has probability density function:
873: \[f_Z(z) = \int_{-\infty}^\infty f_X(x)f_Y(z-x) dx
874: = \int_{-\infty}^\infty f_X(z-x)f_Y(x) dx.\]
875: \end{theorem}
876:
877: %
878: %
879: %
880: %
881: %
882: %
883: %
884: %
885: %
886: %
887: %
888: %
889: %
890: %
891: %
892: %
893: %
894:
895: %
896: %
897: %
898: %
899: %
900: %
901: %
902: %
903: %
904: %
905: %
906: %
907:
908: %
909: %
910: %
911: %
912: %
913: %
914: %
915:
916: %
917: %
918:
919: \subsection{Reliability of long calculations}
920:
921: What we are actually interested in is whether a series of
922: calculations might accumulate a sufficiently large
923: error to become meaningless. In the language we have developed, we are
924: asking what is the probability that all calculations of
925: length upto $n$ is correct:
926: %
927: %
928: $$\Pr\left(\max_{1\le i\le n}(|S_i|)\le\epsilon\right).$$
929:
930: %
931: %
932: %
933:
934: %
935: %
936: %
937: %
938: %
939:
940: %
941:
942: Because they have nice convergence properties, we are especially
943: interested in {\em martingales}
944:
945: \begin{definition}
946: A sequence $\{S_n\}$ is a {\em martingale} with respect to the
947: sequence $\{X_n\}$, if for all $n$:
948: \begin{enumerate}
949: \item $\Ex(|S_n|)<\infty$; and
950: \item $\Ex(S_{n+1};~X_1,~X_2,~\ldots,~X_n) = S_n$
951: \end{enumerate}
952: \end{definition}
953:
954: We first observe that the sequence $S_n=\Sigma_{i=1}^n X_i$ (as
955: previously defined) is a martingale with respect to the sequence
956: $\{X_n\}$.
957: \begin{lemma}
958: The sequence $\{S_n\}$, where $S_n=\sum_{i=1}^n X_i$, and each
959: $X_n$ is an independent random variable with $\Ex(X_n)=0$, is
960: martingale with respect to the sequence $\{X_n\}$.
961: \end{lemma}
962:
963: Alternatively as could be needed for program \ref{lst/ode}:
964:
965: \begin{lemma}
966: The sequence $\{S_n\}$, where $S_n=\sum_{i=1}^n X_i$, and $\{X_n\}$
967: satisfies for all $i$
968: $$
969: \begin{array}{r c l}
970: \Ex(X_i) & = & 0 \\
971: \Ex(X_i;~X_1 \cdots X_{i-1}) & = & 0,
972: \end{array}
973: $$
974: the sequence $\{S_n\}$ is martingale with respect to the sequence
975: $\{X_n\}$.
976: \end{lemma}
977:
978: We now make use of the Doobs-Kolmogorov Inequality presented
979: Figure~\ref{lst/doobs}. The statement of Theorem~\ref{theo/doobs} is
980: deceptively simple. The key as the astute reader will observe is that
981: we have a restricted form of the Doobs-Kolmogorov Inequality in which
982: the sample spaces of the underlying sequence of random variables are
983: identical. This is an artifact of the PVS type system which would
984: require us to prove multiple version of the theorem at each tuple of
985: instantiated types.
986:
987: Although the type system used in PVS is extraordinarily flexible, it
988: is not as malleable as that used by professional mathematicians. To
989: capture mathematics in its entirety using a theorem prover, we would
990: need to dispense with any form of type checking\footnote{A weak form of
991: type consistency is used in category theory, but this is so weak
992: that we can introduce the Russel Paradox.}. For its intended use as
993: an aide to proving programs correct, this would fatally weaken PVS as
994: a useful tool. In addition, in many practice areas of mathematics, the
995: full generality of categorical constructs is an unnecessary luxury,
996: albeit one with a seductive, siren-like, appeal.
997:
998: %
999:
1000: \begin{figure*}
1001: \begin{center}\fbox{\begin{minipage}{0.98\linewidth}
1002: {\footnotesize \input{doobs}}
1003: \end{minipage}}\end{center}
1004: \caption{Doobs-Kolmogorov inequality in PVS}
1005: \label{lst/doobs}
1006: \end{figure*}
1007:
1008: \begin{theorem}[Doobs-Kolmogorov Inequality]
1009: \label{theo/doobs}
1010: If $\{S_n\}$ is a martingale with respect to $\{X_n\}$ then,
1011: provided that $\epsilon>0$:
1012: \[\Pr\left(\max_{1\le i\le n}(|S_i|)\ge\epsilon\right)
1013: \le \frac{1}{{\epsilon}^2} \Ex(S_n^2)\]
1014: \end{theorem}
1015:
1016: In our particular case where each $X_i$ is an independent random
1017: variable with $\Ex(X_i)=0$, and $\mbox{Var}(X_i)=\sigma_i^2$, we
1018: observe that
1019: $$
1020: \Pr\left(\max_{1\le i\le n}(|S_i|)\le\epsilon\right)
1021: \ge 1-\frac{1}{{\epsilon}^2}\sum_{i=1}^n\sigma_i^2
1022: $$
1023:
1024: The short conclusion is therefore that eventually errors will
1025: accumulate and overwhelm the accuracy of any numerical software.
1026: However, if $\epsilon$ is large enough and each of the $\sigma_i^2$
1027: are small enough, then the number of iterations required for this to
1028: occur will be high enough to be of no practical significance.
1029: Crucially, the results hinge critically on the errors $\{X_n\}$ being
1030: independent.
1031:
1032: %
1033:
1034: %
1035: %
1036: %
1037:
1038: %
1039: %
1040: %
1041:
1042: %
1043: %
1044: %
1045: %
1046: %
1047: %
1048: %
1049: %
1050:
1051: %
1052: %
1053:
1054: %
1055:
1056: %
1057: %
1058: %
1059: %
1060:
1061:
1062: %
1063: %
1064: %
1065: %
1066: %
1067: %
1068:
1069: %
1070: %
1071: %
1072: %
1073: %
1074: %
1075:
1076: %
1077: %
1078: %
1079: %
1080: %
1081: %
1082:
1083: %
1084:
1085:
1086: %
1087: %
1088: %
1089: %
1090:
1091:
1092: %
1093: %
1094: %
1095: %
1096: %
1097: %
1098: %
1099: %
1100: %
1101:
1102:
1103: %
1104: %
1105: %
1106:
1107:
1108: %
1109: %
1110: %
1111:
1112: %
1113: %
1114: %
1115: %
1116: %
1117: %
1118: %
1119: %
1120: %
1121: %
1122: %
1123: %
1124:
1125:
1126: %
1127: %
1128: %
1129: %
1130: %
1131: %
1132: %
1133: %
1134: %
1135: %
1136: %
1137: %
1138: %
1139: %
1140: %
1141: %
1142: %
1143: %
1144: %
1145:
1146:
1147:
1148: %
1149: %
1150: %
1151: %
1152: %
1153: %
1154: %
1155: %
1156: %
1157: %
1158: %
1159: %
1160: %
1161: %
1162: %
1163: %
1164: %
1165: %
1166: %
1167: %
1168: %
1169: %
1170:
1171: \section{Future work}
1172:
1173: This work will be continued in two directions. The first direction is
1174: to modify Fluctuat to generate theorems that can be checked
1175: automatically by PVS using
1176: ProofLite\footnote{\url{http://research.nianet.org/~munoz/ProofLite/}.}
1177: as proposed in \cite{DauMelMun05,MunLes05}. This work will be carried
1178: in collaboration with the developers of Fluctuat. The software will
1179: conservatively estimate the final effect of the error introduces by
1180: each individual floating point operations and compute upper bounds of
1181: their variances.
1182:
1183: The second direction is to develop and check accurate proofs about the
1184: round-off errors of individual equations. A uniformly distributed
1185: random variable whose variance depends only on the operation and the
1186: computed result might provide a too pessimistic bound. For example the
1187: floating point addition of a large number with a small number absorbs
1188: the small number meaning that the round-off error may be far below
1189: half an ulp of the computed result.
1190:
1191: Two's complement operation of TMS320 circuit can either round or
1192: truncate the result. If truncation is used, it introduces a drift and
1193: Doobs-Kolmogorov inequality for martingales cannot be used. Should we
1194: wish to extend this work to account for drifts (non-zero means for the
1195: random variables $\{X_n\}$), then we anticipate making use of Wald
1196: Identity. Such developments will also be necessary to address higher
1197: order error terms that introduce a drift.
1198:
1199: This library and future work will be included into NASA Langley PVS
1200: library\footnote{\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html}.}
1201: as soon as it becomes stable.
1202:
1203: We saw with the example of listing~\ref{lst/ode} that inductions on
1204: the variances of the random variables can be crudely bounded. Yet, we
1205: may expect tighter results if we use tools that are able to infer
1206: inductions and solve them mathematically but this domain is far from
1207: the authors' research areas.
1208:
1209: \section{Conclusions}
1210:
1211: To the best of our knowledge this paper presents the first application
1212: of the Doobs-Kolmogorov Inequality to software reliability and the
1213: first generic formal development able to handle continuous, discrete
1214: and non-continuous non-discrete random variable for PVS. Previous
1215: developments in higher order logic where targeting other applications
1216: and using Coq, HOL or Mizar proof assistants (see \cite{Hur02,AudPau06} and
1217: references herein). In addition, we have demonstrated a slightly
1218: weaker version of this result in PVS. We claim that the utility of
1219: this weaker result is not unduly restrictive, when compared to the
1220: general result. The major restriction lies in the fact that we have to
1221: demonstrate that a sequence of overall errors is martingale with
1222: respect to the sequence of individual errors. We have been forced to
1223: make simplifications to the mathematical model of our software to
1224: ensure that this is the case. In particular, we have been forced to
1225: insist that our individual errors have no drift, and are independent.
1226:
1227: We have been surprised that the limit on the reliability of a piece of
1228: numeric software could be expressed so succinctly. Notice that even
1229: with a high tolerance of error, and with independent errors, we will
1230: still eventually fail. Our results permit the development of safe upper
1231: limits on the number of operations that a piece of numeric software
1232: should be permitted to undertake.
1233:
1234: It is worth pointing out that violating our assumptions (independence
1235: of errors, and zero drift) would lead to worse results, so one should
1236: treat the limits we have deduced with caution, should these
1237: assumptions not be met.
1238:
1239: %
1240:
1241: %
1242: \section*{Acknowledgment}
1243: %
1244: %
1245:
1246: This work has been partially funded by CNRS PICS 2533 and was
1247: partially done while one of the authors was an invited professor at
1248: the University of Perpignan Via Domitia. It benefits from links
1249: between the École Normale Supérieure de Lyon where one
1250: author used to work and the University of Manchester started in the
1251: Mathlogaps multi-participant Early Stage Research Training network of
1252: the European Union. The authors would like to thanks Philippe Langlois,
1253: Harold Simmons and Jean-Marc Vincent for fruitful informal discussions
1254: on this work.
1255:
1256: %
1257: %
1258: %
1259: %
1260: %
1261: %
1262: %
1263:
1264: %
1265: %
1266: %
1267:
1268: %
1269: %
1270: %
1271: \bibliographystyle{IEEEtran.bst}
1272: %
1273: %
1274: \bibliography{alias,perso,groupe,saao,these,livre,arith}
1275:
1276: %
1277: %
1278: %
1279: %
1280:
1281: %
1282:
1283: %
1284: %
1285: %
1286:
1287: %
1288:
1289:
1290: %
1291:
1292:
1293: \end{document}
1294: