Naslov
Predicate Abstraction in Protocol Verification

Autori
Pek, Edgar ; Bogunović, Nikola

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 8th International Conference on Telecomunications / Gledec, Gordan ; Ježić, Gordan - Zagreb : Fakultet elektrotehnike i računarstva Sveučilišta u Zagrebu, 2005, 627-632

Skup
8th International Conference on Telecommunications

Mjesto i datum
Zagreb, Hrvatska, 15.06.2005. - 17.06.2005

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
formal verification; abstract interpretation; model checking; theorem proving; predicate abstraction

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo

POVEZANOST RADA