Validation of Embedded Systems using Formal Method aided Verification
8th Euromicro Conference on Digital System Design (DSD'2005), Porto, Portugal, August 30 - September 3, 2005, pp. 196-199
Informal validation techniques, such as simulation, suffer from the fact that they only examine a small fraction of the state space. Formal techniques, on the other hand, suffer from state space explosion and are not practical to use for huge, complex systems. This paper proposes a validation approach, based on simulation, which addresses some of the above problems. Formal methods, in particular model checking, are used to aid the simulation process in certain situations in order to boost coverage. The invocation frequency of the model checker is dynamically controlled by estimating certain parameters, based on statistics collected previously during the same validation session, in order to minimise verification time and at the same time achieve reasonable coverage. The approach has been demonstrated feasible by numerous experimental results.
[KEP05] Daniel Karlsson, Petru Eles, Zebo Peng, "Validation of Embedded Systems using Formal Method aided Verification", 8th Euromicro Conference on Digital System Design (DSD'2005), Porto, Portugal, August 30 - September 3, 2005, pp. 196-199