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
Verification of Component-based Embedded System Designs
Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory. Linköping University, The Institute of Technology.
2006 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components. At the same time, the systems must fulfill strict functional and non-functional requirements.

This thesis presents novel and efficient techniques for the verification of component-based embedded system designs. As a common basis, these techniques have been developed using a Petri net based modelling approach, called PRES+.

Two complementary problems are addressed: component verification and integration verification. With component verification the providers verify their components so that they function correctly if given inputs conforming to the assumptions imposed by the components on their environment.

Two techniques for component verification are proposed in the thesis. The first technique enables formal verification of SystemC designs by translating them into the PRES+ representation. The second technique involves a simulation based approach into which formal methods are injected to boost verification efficiency.

Provided that each individual component is verified and is guaranteed to function correctly, the components are interconnected to form a complete system. What remains to be verified is the interface logic, also called glue logic, and the interaction between components.

Each glue logic and interface cannot be verified in isolation. It must be put into the context in which it is supposed to work. An appropriate environment must thus be derived from the components to which the glue logic is connected. This environment must capture the essential properties of the whole system with respect to the properties being verified. In this way, both the glue logic and the interaction of components through the glue logic are verified. The thesis presents algorithms for automatically creating such environments as well as the underlying theoretical framework and a step-by-step roadmap on how to apply these algorithms.

Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2006. , 294 p.
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1017
Keyword [en]
Datorsystem, embedded systems, formal verification, Petri-net, IP, reuse, components, model checking, simulation
Keyword [sv]
Datorsystem
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:liu:diva-7473ISBN: 91-85523-79-8 (print)OAI: oai:DiVA.org:liu-7473DiVA: diva2:22478
Public defence
2006-06-19, Visionen, Hus B, Campus Valla, Linköpings universitet, Linköping, 10:15 (English)
Opponent
Supervisors
Available from: 2006-09-28 Created: 2006-09-28 Last updated: 2009-11-25Bibliographically approved

Open Access in DiVA

fulltext(4072 kB)916 downloads
File information
File name FULLTEXT01.pdfFile size 4072 kBChecksum MD5
a5c8395f814f571d126ae98e524948aecea4d961f9340b79e34dd02093f63f122f2d982e
Type fulltextMimetype application/pdf

Other links

Link to Licentiate Thesis

Authority records BETA

Karlsson, Daniel

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 916 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: 1654 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