Stochastic Formal Methods for Hybrid Systems
<|reference_start|>Stochastic Formal Methods for Hybrid Systems: 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\'evy'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.<|reference_end|>
@article{daumas2006stochastic,
    title={Stochastic Formal Methods for Hybrid Systems},
    author={Marc Daumas (ELIAUS), David Lester (University of Manchester), Erik
  Martin-Dorel (ELIAUS, Lamps), Annick Truffert (LAMPS)},
    journal={arXiv preprint arXiv:cs/0610110},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0610110},
    primaryClass={cs.MS}
}