Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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
Application and. verification of local nonsemantic-preserving transformations in system-design
KTH, School of Information and Communication Technology (ICT), Electronic, Computer and Software Systems, ECS.
KTH, School of Information and Communication Technology (ICT), Electronic, Computer and Software Systems, ECS.ORCID iD: 0000-0003-4859-3100
KTH, School of Information and Communication Technology (ICT), Electronic, Computer and Software Systems, ECS.
2008 (English)In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, ISSN 0278-0070, E-ISSN 1937-4151, Vol. 27, no 6, 1091-1103 p.Article in journal (Refereed) Published
Abstract [en]

Due to the increasing abstraction gap between the initial system model and a final implementation, the verification of the respective models against each other is a formidable task. This paper addresses the verification problem by proposing a stepwise application of combined refinement and verification activities in the context of synchronous model of computation. An implementation model is developed from the system model by applying pre-defined design transformations which are as follows: 1) semantic preserving or 2) nonsemantic preserving. Nonsemantic-preserving transformations introduce lower level implementation details, which are necessary to yield an efficient implementation. Our approach divides the verification tasks into two activities: 1) the local correctness of a refined block is checked by using formal verification tools and predefined properties, which are developed for each nonsemantic-preserving transformation, and 2) the global influence of the refinement to the entire system is studied through static analysis. We illustrate the design refinement and verification approach with three transformations: 1) a communication refinement mapping a synchronous channel to an asynchronous one including a handshake mechanism; 2) a computation refinement, which introduces resource sharing in a combinational computation block; and 3) a synchronization demanding refinement, where an algorithm analyzes the influence of a local refinement to the temporal properties of the entire system and restores the system's correct temporal behavior if necessary.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2008. Vol. 27, no 6, 1091-1103 p.
Keyword [en]
Design refinement, Formal verification, Synchronization, System design
National Category
Embedded Systems
Identifiers
URN: urn:nbn:se:kth:diva-17555DOI: 10.1109/tcad.2008.923249ISI: 000256156400009Scopus ID: 2-s2.0-44149107365OAI: oai:DiVA.org:kth-17555DiVA: diva2:335599
Note

QC 20100525

Available from: 2010-08-05 Created: 2010-08-05 Last updated: 2017-12-12Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Sander, Ingo

Search in DiVA

By author/editor
Raudvere, TarvoSander, IngoJantsch, Axel
By organisation
Electronic, Computer and Software Systems, ECS
In the same journal
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 84 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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