Linköping University: Students Alumni Trade and Industry/Society Internal Search
danka_dsd05

Validation of Embedded Systems using Formal Method aided Verification

Daniel Karlsson
 
Petru Eles Author homepage
Zebo Peng Author homepage

8th Euromicro Conference on Digital System Design (DSD'2005), Porto, Portugal, August 30 - September 3, 2005, pp. 196-199

ABSTRACT
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.


Related files:
danka_dsd05.final.pdf, Adobe Acrobat portable document


[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
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)