Predicate Abstraction in Protocol Verification (CROSBI ID 507033)
Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Pek, Edgar ; Bogunović, Nikola
engleski
Predicate Abstraction in Protocol Verification
This paper presents how predicate abstraction can be applied to protocol verification. Predicate abstraction is a method for automatic construction of abstract state graph. Basic idea is to use $n$ predicates defined on concrete state space to generate abstract state graph. Model checking is a formal verification technique which has been successfully applied to protocol verification. But model checking can only be applied to finite state systems. Many interesting systems are infinite state or number of states is so large that verification becomes infeasible. Predicate abstraction can be applied in verification of infinite state systems (or large finite state systems). Abstract state graph created by predicate abstraction can be used for verification of safety properties using a model checker. We provide simple examples of protocol verification using predicate abstraction.
formal verification; abstract interpretation; model checking; theorem proving; predicate abstraction
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
627-632-x.
2005.
objavljeno
Podaci o matičnoj publikaciji
Proceedings of the 8th International Conference on Telecomunications
Gledec, Gordan ; Ježić, Gordan
Zagreb: Fakultet elektrotehnike i računarstva Sveučilišta u Zagrebu
Podaci o skupu
8th International Conference on Telecommunications
predavanje
15.06.2005-17.06.2005
Zagreb, Hrvatska