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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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.
Series
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
Identifiers
URN: urn:nbn:se:liu:diva-5696ISBN: 91-7373-787-9 (print)OAI: oai:DiVA.org:liu-5696DiVA: diva2:21460
Presentation
2003-12-11, 00:00 (English)
Supervisors
Note
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)500 downloads
File information
File name FULLTEXT01.pdfFile size 1329 kBChecksum MD5
bb2ce9068b1be64617db1a3f79dbaecbbf4f3931eb8247425b88f9f0818a3650bb6a2ac5
Type fulltextMimetype application/pdf

Other links

Link to Ph.D. Thesis

Authority records BETA

Karlsson, Daniel

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: 500 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

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 419 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf