Symbolic simulation of synchronous programs
David Garriou · Electronic Notes in Theoretical Computer Science · 2002
This paper proposes an intermediate approach between simulation and formal verification. This method called symbolic simulation allows to simulate a reactive program by giving it the set of its possible inputs. An important aspect of this work is the fact that we deal with values of unbounded numerical variables and take them into account while computing properties of control. This has been done for synchronous languages, (e.g. Lustre, Esterel and Signal), as these languages are known to provide precise mathematical description of critical embedded systems with real time constraints.