Towards Formal Verification in a Component-based Reuse Methodology
2003 (English)Licentiate thesis, monograph (Other academic)
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.
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.
The verification methodology as well as the underlying theoretical framework and algorithms are presented in the thesis.
Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply it on real-life examples.
Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2003. , 187 p.
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 1058
Formal verification, Model checking, Petri net, Reuse
IdentifiersURN: urn:nbn:se:liu:diva-5696ISBN: 91-7373-787-9OAI: oai:DiVA.org:liu-5696DiVA: diva2:21460
2003-12-11, 00:00 (English)
Eles, PetruPeng, Zebo
Report code: LiU-Tek-Lic-2003:57.2003-12-052003-12-052009-05-22