混合系统的随机形式方法
摘要：通过给出一个框架来限定杂合系统累积误差从未超过给定阈值的概率。此类系统用于模拟飞机或核电站等实体系统及其软件。本报告基于Lévy和Markov的不等式提供简单公式，并提出随机变量的形式理论，特别关注产生具体结果。我们选择了四种非常常见的应用程序，适用于我们的框架，并涵盖演化时间较长的混合系统的常见实践。我们计算前两种应用程序中持续保持显著位数的比特数，其失效概率约为十亿分之一，而最坏情况分析则认为没有显著位数保留。我们使用PVS作为此类形式化工具，以强制明确陈述所有假设，并防止定理的错误使用。
作者：Marc Daumas (ELIAUS), David Lester (University of Manchester), Erik Martin-Dorel (ELIAUS, Lamps), Annick Truffert (LAMPS)
论文ID：cs/0610110
分类：Mathematical Software
分类简称：cs.MS
提交时间：2009-02-24