Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs
Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs
复制标题
从反应式程序的动态观察中自动合成规范
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Patrice Godefroid
中科院分区：
文献类型：
--
作者：
Bernard Boigelot;Patrice Godefroid
VeriSoft[God97]是一个工具，用于系统地探索由执行任意C(或C++)代码的多个并发进程组成的系统的状态空间。VeriSoft可以自动检测系统并发进程之间的协调问题。在本文中，我们提出了一种方法来综合有限状态机，该有限状态机模拟在VeriSoft执行的状态空间探索期间观察到的给定进程的所有可视操作序列。通过对这台机器的检查，可以发现进程在其环境中的动态行为，并了解它如何对系统的全局行为做出贡献。
VeriSoft [God97] is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C (or C++) code. VeriSoft can automatically detect coordination problems between the concurrent processes of a system. In this paper, we present a method to synthesize a finite-state machine that simulates all the sequences of visible operations of a given process that were observed during a state-space exploration performed by VeriSoft. The examination of this machine makes it possible to discover the dynamic behavior of the process in its environment and to understand how it contributes to the global behavior of the system.