Change search
ReferencesLink to record
Permanent link

Direct link
System Level Techniques for Verification and Synchronization after Local Design Refinements
KTH, School of Information and Communication Technology (ICT), Electronic, Computer and Software Systems, ECS.
2007 (English)Doctoral thesis, monograph (Other scientific)
Abstract [en]

Today's advanced digital devices are enormously complex and incorporate many functions. In order to capture the system functionality and to be able to analyze the needs for a final implementation more efficiently, the entry point of the system development process is pushed to a higher level of abstraction. System level design methodologies describe the initial system model without considering lower level implementation details and the objective of the design development process is to introduce lower level details through design refinement.

In practice this kind of refinement process may entail non-semantic-preserving changes in the system description, and introduce new behaviors in the system functionality. In spite of new behaviors, a model formed by the refinement may still satisfy the design constraints and to realize the expected system. Due to the size of the involved models and the huge abstraction gap, the direct verification of a detailed implementation model against the abstract system model is quite impossible. However, the verification task can be considerably simplified, if each refinement step and its local implications are verified separately. One main idea of the Formal System Design (ForSyDe) methodology is to break the design process into smaller refinement steps that can be individually understood, analyzed and verified.

The topic of this thesis is the verification of refinement steps in ForSyDe and similar methodologies. It proposes verification attributes attached to each non-semantic-preserving transformation. The attributes include critical properties that have to be preserved by transformations. Verification properties are defined as temporal logic expressions and the actual verification is done with the SMV model checker. The mapping rules of ForSyDe models to the SMV language are provided. In addition to properties, the verification attributes include abstraction techniques to reduce the size of the models and to make verification tractable. For computation refinements, the author defines the polynomial abstraction technique, that addresses verification of DSP applications at a high abstraction level. Due to the size of models, predefined properties target only the local correctness of refined design blocks and the global influence has to be examined separately. In order to compensate the influence of temporal refinements, the thesis provides two novel synchronization techniques. The proposed verification and synchronization techniques have been applied to relevant applications in the computation area and to communication protocols.

Place, publisher, year, edition, pages
Stockholm: KTH , 2007. , xiv, 155 p.
Trita-ICT-ECS AVH, ISSN 1653-6363 ; 2007:05
Keyword [en]
Electronic System Design, Refinement, Verification, Synchronization
National Category
Information Science
URN: urn:nbn:se:kth:diva-4471ISBN: 978-91-7178-677-7OAI: diva2:12420
Public defence
2007-09-11, Sal D, Forum, Isafjordsgatan 39, Kista, 13:00
QC 20100816Available from: 2007-08-23 Created: 2007-08-23 Last updated: 2010-08-16Bibliographically approved

Open Access in DiVA

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

Search in DiVA

By author/editor
Raudvere, Tarvo
By organisation
Electronic, Computer and Software Systems, ECS
Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 359 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: 512 hits
ReferencesLink to record
Permanent link

Direct link