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

Model Validation for Embedded Systems Using Formal Method-Aided Simulation

Daniel Karlsson
 
Petru Eles Author homepage
Zebo Peng Author homepage

IET Computers & Digital Techniques journal, Vol. 2, Number 6, November 2008, pp. 413-433.

ABSTRACT
Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex. At the same time, the systems must fulfill strict requirements on reliability and correctness. Informal validation techniques, such as simulation, suffer from the fact that they only examine a small fraction of the state space. Therefore, simulation results cannot be 100% guaranteed. Formal techniques, on the other hand, suffer from state space explosion and might not be practical for huge, complex systems due to memory and time limitations. 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, or guide, 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 related to the simulation speed of the particular system at hand. These estimations are based on statistical data collected during the validation session, in order to minimise verification time, and at the same time, achieve reasonable coverage.


Related files:
danka_iet08.pdfAdobe Acrobat portable document


[KEP08] Daniel Karlsson, Petru Eles, Zebo Peng, "Model Validation for Embedded Systems Using Formal Method-Aided Simulation", IET Computers & Digital Techniques journal, Vol. 2, Number 6, November 2008, pp. 413-433.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)