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

Formal Coverification of Embedded Systems using Model Checking

Luis Alejandro Cortes
 
Petru Eles Author homepage
Zebo Peng Author homepage

26th Euromicro Conference (Digital Systems Design), Maastricht, The Netherlands, Sept. 5-7, 2000, vol. I, pp. 106-113.

ABSTRACT
The complexity of embedded systems is increasing rapidly. In consequence, new verification techniques that overcome the limitations of traditional methods and are suitable for hardware/software systems are needed. In this paper we introduce a computational model for embedded systems based on Petri nets, called PRES. We present an approach to coverification of both the hardware and software parts of an embedded system represented by PRES. We use symbolic model checking to prove the correctness of such systems, specifying properties in CTL and verifying whether they are satisfied. This coverification method permits to reason formally about design properties as well as timing requirements. A medical monitoring system illustrates the feasibility of our approach on practical applications.


Related files:
EUROMICRO00.pdfAdobe Acrobat portable document
EUROMICRO00.ps.gzpostscript document, compressed (with gzip)


[AEP00] Luis Alejandro Cortes, Petru Eles, Zebo Peng, "Formal Coverification of Embedded Systems using Model Checking", 26th Euromicro Conference (Digital Systems Design), Maastricht, The Netherlands, Sept. 5-7, 2000, vol. I, pp. 106-113.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)