Abstract :
[en] VeriSoft 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.
Scopus citations®
without self-citations
7