Automatic Verification of Parameterized Systems by Over-Approximation
2015 (English)Licentiate thesis, monograph (Other academic)
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
Computer Science Software Engineering
IdentifiersURN: 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
2015-12-11, Alan Turing, hus E, Campus Valla, Linköpings universitet, Linköping, 13:15 (English)
Seceleanu, Cristina, Docent
Nilsson, Ulf, Professor