liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Towards Formal Verification in a Component-based Reuse Methodology
Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
2003 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

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
Keyword [en]
Formal verification, Model checking, Petri net, Reuse
National Category
Computer Science
URN: urn:nbn:se:liu:diva-5696ISBN: 91-7373-787-9OAI: diva2:21460
2003-12-11, 00:00 (English)
Report code: LiU-Tek-Lic-2003:57.Available from: 2003-12-05 Created: 2003-12-05 Last updated: 2009-05-22

Open Access in DiVA

fulltext(1329 kB)455 downloads
File information
File name FULLTEXT01.pdfFile size 1329 kBChecksum SHA-1
Type fulltextMimetype application/pdf

Other links

Link to Ph.D. Thesis

Search in DiVA

By author/editor
Karlsson, Daniel
By organisation
ESLAB - Embedded Systems LaboratoryThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 455 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 389 hits
ReferencesLink to record
Permanent link

Direct link