静态模型检验中的抽象与精化
Abstraction and Refinement in Static Model-Checking
摘要：
解释是建立程序的静态分析的一般方法。它是由P.和R. \cite{cc}中的Cousot。在本文中，我们提出了一个通用的抽象解释领域的模型检验的应用。动态检查通常更容易使用，因为它的概念已经建立并且广为人知。但它们通常仅限于状态空间有限的系统。在另一部分，某些故障不能动态检测，即使通过跟踪状态空间的历史。事实上，寻找正确的测试用例的经典问题是远远不够的，并进一步限制了动态检查器的能力。静态检查的优点是它们比动态检查器工作在更抽象的级别上，并且可以验证所有输入的系统属性。问题，很难保证对模型属性的违反对应于具体系统中的故障。我们提出了一种方法，在该方法中，我们动态生成反例使用的抽象解释技术。
英文摘要：
interpretation is a general methodology for building static analyses of programs. It was introduced by P. and R. Cousot in \cite{cc}. We present, in this paper, an application of a generic abstract interpretation to domain of model-checking. Dynamic checking are usually easier to use, because the concept are establishe d and wide well know. But they are usually limited to systems whose states space is finite. In an other part, certain faults cannot be detected dynamically, even by keeping track of the history of the states space.Indeed, the classical problem of finding the right test cases is far from trivial and limit the abilities of dynamic checkers further. Static checking have the advantage that they work on a more abstract level than dynamic checker and can verify system properties for all inputs. Problem, it is hard to guarantee that a violation of a modeled property corresponds to a fault in the concrete system. We propose an approach, in which we generate counter-examples dynamically using the abstract interpretation techniques.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
