Sökning: id:"swepub:oai:DiVA.org:hh-19670" >
Automatic Verificat...
Automatic Verification of Parameterized Systems by Over-Approximation
-
- Jahundovics, Vladislavs, 1978- (författare)
- Linköpings universitet,Institutionen för datavetenskap,Tekniska fakulteten
-
- Nilsson, Ulf, Professor (preses)
- Linköpings universitet,Programvara och system,Tekniska fakulteten
-
- Seceleanu, Cristina, Docent (opponent)
- Division of Embedded Systems, Mälardalen University, Sweden
-
(creator_code:org_t)
- ISBN 9789176859186
- 2015-11-17
- Engelska 155 s.
-
Serie: Linköping Studies in Science and Technology. Thesis, 0280-7971 ; 1732
- Relaterad länk:
-
https://liu.diva-por... (primary) (Raw object)
-
visa fler...
-
https://liu.diva-por...
-
https://liu.diva-por... (Preview)
-
http://liu.diva-port...
-
https://urn.kb.se/re...
-
https://doi.org/10.3...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Software Engineering (hsv//eng)
Publikations- och innehållstyp
- vet (ämneskategori)
- lic (ämneskategori)
Hitta via bibliotek
Till lärosätets databas