Change search
ReferencesLink to record
Permanent link

Direct link
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.
Linköping Studies in Science and Technology. Thesis, ISSN 0280-7971 ; 1732
National Category
Computer Science Software Engineering
URN: urn:nbn:se:liu:diva-121776DOI: 10.3384/diss.diva-121776ISBN: 978-91-7685-918-6 (print)OAI: diva2:871844
2015-12-11, Alan Turing, hus E, Campus Valla, Linköpings universitet, Linköping, 13:15 (English)
Available from: 2015-11-17 Created: 2015-10-05 Last updated: 2015-11-17Bibliographically approved

Open Access in DiVA

fulltext(4629 kB)69 downloads
File information
File name FULLTEXT01.pdfFile size 4629 kBChecksum SHA-512
Type fulltextMimetype application/pdf
omslag(53 kB)10 downloads
File information
File name COVER01.pdfFile size 53 kBChecksum SHA-512
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: 69 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

Altmetric score

Total: 931 hits
ReferencesLink to record
Permanent link

Direct link