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
Formal verification of component-based designs
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
Linköping University, The Institute of Technology. Linköping University, Department of Computer and Information Science, ESLAB - Embedded Systems Laboratory.
2007 (English)In: Design automation for embedded systems, ISSN 0929-5585, E-ISSN 1572-8080, Vol. 11, no 1, 49-90 p.Article in journal (Refereed) Published
Abstract [en]

Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex, and designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must fulfill strict requirements on reliability and correctness. This paper 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 them already formally verified by their designers. The components are considered correct given that the environment satisfies certain properties imposed by the component. The methodology verifies the correctness of the glue logic inserted between the components and the interaction of the components through the glue logic. Each such glue logic is verified one at a time using model checking techniques. Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply such a verification methodology on real-life examples. © Springer Science + Business Media, LLC 2006.

Place, publisher, year, edition, pages
2007. Vol. 11, no 1, 49-90 p.
Keyword [en]
Components, Embedded systems, Formal verification, IP, Model checking, Petri-nets, Real-time systems
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:liu:diva-49986DOI: 10.1007/s10617-006-9723-3OAI: oai:DiVA.org:liu-49986DiVA: diva2:270882
Available from: 2009-10-11 Created: 2009-10-11 Last updated: 2017-12-12

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Karlsson, DanielEles, Petru IonPeng, Zebo

Search in DiVA

By author/editor
Karlsson, DanielEles, Petru IonPeng, Zebo
By organisation
The Institute of TechnologyESLAB - Embedded Systems Laboratory
In the same journal
Design automation for embedded systems
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 143 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