<p>Embedded systems are becoming increasingly common in our everyday lives. As techonology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must still fulfill strict requirements on reliability and correctness.</p><p>This thesis 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 these components are already formally verified by their designers and are considered correct given that the environment satisfies certain properties imposed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified one at a time using model checking techniques.</p><p>The verification methodology as well as the underlying theoretical framework and algorithms are presented in the thesis.</p><p>Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply it on real-life examples.</p> / Report code: LiU-Tek-Lic-2003:57.
| Identifer | oai:union.ndltd.org:UPSALLA/oai:DiVA.org:liu-5696 |
| Date | January 2003 |
| Creators | Karlsson, Daniel |
| Publisher | Linköping University, Linköping University, ESLAB - Embedded Systems Laboratory, Institutionen för datavetenskap |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Licentiate thesis, monograph, text |
| Relation | Linköping Studies in Science and Technology. Thesis, 0280-7971 ; 1058 |
Page generated in 0.0017 seconds