danka_acm_design07

Formal Verification of Component-based Designs

Daniel Karlsson Author homepage
 
Petru Eles Author homepage
Zebo Peng Author homepage

Journal of Design Automation for Embedded Systems, Vol. 11, No. 1, March 2007, pp. 49-90

ABSTRACT
Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex, and designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must fulfill strict requirements on reliability and correctness.

This paper proposes a formal verification methodology which smoothly integrates with component-based system-level design using a divide and conquer approach. The methodology assumes that the system consists of several reusable components, each of them already formally verified by their designers. The components are considered correct given that the environment satisfies certain properties imposed by the component. The methodology verifies the correctness of the glue logic inserted between the components and the interaction of the components through the glue logic. Each such glue logic is verified one at a time using model checking techniques. Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply such a verification methodology on real-life examples.


Related files:
danka_acm_design07.pdfAdobe Acrobat portable document


[KEP07] Daniel Karlsson, Petru Eles, Zebo Peng, "Formal Verification of Component-based Designs", Journal of Design Automation for Embedded Systems, Vol. 11, No. 1, March 2007, pp. 49-90
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)
Last modified on Monday December 04, 2006 by Gert Jervan