Stochastic Formal Methods for Hybrid Systems
| dc.creator | Daumas, Marc | |
| dc.creator | Lester, David | |
| dc.creator | Martin-Dorel, Erik | |
| dc.creator | Truffert, Annick | |
| dc.date | 2006-10-18 | |
| dc.date | 2009-02-24 | |
| dc.date.accessioned | 2026-07-07T12:45:54Z | |
| dc.date.available | 2026-07-07T12:45:54Z | |
| dc.description | We provide a framework to bound the probability that accumulated errors were never above a given threshold on hybrid systems. Such systems are used for example to model an aircraft or a nuclear power plant on one side and its software on the other side. This report contains simple formulas based on Lévy's and Markov's inequalities and it presents a formal theory of random variables with a special focus on producing concrete results. We selected four very common applications that fit in our framework and cover the common practices of hybrid 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 against 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. | |
| dc.identifier | https://arxiv.org/abs/cs/0610110 | |
| dc.identifier | http://arxiv.org/abs/cs/0610110 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/221206 | |
| dc.subject | Mathematical Software | |
| dc.title | Stochastic Formal Methods for Hybrid Systems | |
| dc.type | text |