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
Automatic Verification of Parameterized Systems by Over-Approximation
Linköping University, Department of Computer and Information Science. Linköping University, Faculty of Science & Engineering.
2015 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

This thesis presents a completely automatic verification framework to check safety properties of parameterized systems. A parameterized system is a family of finite state systems where every system consists of a finite number of processes running in parallel the same algorithm. All the systems in the family differ only in the number of the processes and, in general, the number of systems in a family may be unbounded. Examples of parameterized systems are communication protocols, mutual exclusion protocols, cache coherence protocols, distributed algorithms etc.

Model-checking of finite state systems is a well-developed formal verification approach of proving properties of systems in an automatic way. However, it cannot be applied directly to parameterized systems because the unbounded number of systems in a family means an infinite state space. In this thesis we propose to abstract an original family of systems consisting of an unbounded number of processes into one consisting of a fixed number of processes. An abstracted system is considered to consist of k+1 components—k reference processes and their environment. The transition relation for the abstracted system is an over-approximation of the transition relation for the original system, therefore, a set of reachable states of the abstracted system is an over-approximation of the set of reachable states of the original one.

A safety property is considered to be parameterized by a fixed number of processes whose relationship is in the center of attention in the property. Such processes serve as reference processes in the abstraction. We propose an encoding which allows to perform reachability analysis for an abstraction parameterized by the reference processes.

We have successfully verified three classic parameterized systems with replicated processes by applying this method.

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 2015. , 155 p.
Series
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 1732
National Category
Computer Science Software Engineering
Identifiers
URN: urn:nbn:se:liu:diva-121776DOI: 10.3384/diss.diva-121776ISBN: 978-91-7685-918-6 (print)OAI: oai:DiVA.org:liu-121776DiVA: diva2:871844
Presentation
2015-12-11, Alan Turing, hus E, Campus Valla, Linköpings universitet, Linköping, 13:15 (English)
Opponent
Supervisors
Available from: 2015-11-17 Created: 2015-10-05 Last updated: 2015-11-17Bibliographically approved

Open Access in DiVA

fulltext(4629 kB)137 downloads
File information
File name FULLTEXT01.pdfFile size 4629 kBChecksum SHA-512
039a1d5bd31628bc4b612264d0e85bf273598225d266b9f875003e929e1735c0b33a894e70c42d01ef7ecb5dfc422deb5b3d547d14e6afd30b72ee57d2ec687d
Type fulltextMimetype application/pdf
omslag(53 kB)13 downloads
File information
File name COVER01.pdfFile size 53 kBChecksum SHA-512
b4716c5e903d6cd414697bac1f4665e04074f548a9c1d029df3d6b126aa027471a812aef169174bd60043ad5ed030d1df2e4cd447d12b80833bfb66db6338edd
Type coverMimetype application/pdf

Other links

Publisher's full text
By organisation
Department of Computer and Information ScienceFaculty of Science & Engineering
Computer ScienceSoftware Engineering

Search outside of DiVA

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

doi
isbn
urn-nbn

Altmetric score

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