Pregled bibliografske jedinice broj: 139879
Verification of mutual exclusion algorithms with SMV system
Verification of mutual exclusion algorithms with SMV system // Eurocon 2003, Computer as a tool, Proceedings Volume II / Zajc, Baldomir ; Tkalčić, Marko (ur.).
Piscataway (NJ): Institute of Electrical and Electronics Engineers (IEEE), 2003. str. 12-25 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
CROSBI ID: 139879 Za ispravke kontaktirajte CROSBI podršku putem web obrasca
Naslov
Verification of mutual exclusion algorithms with SMV system
Autori
Bogunović, Nikola ; Pek, Edgar
Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni
Izvornik
Eurocon 2003, Computer as a tool, Proceedings Volume II
/ Zajc, Baldomir ; Tkalčić, Marko - Piscataway (NJ) : Institute of Electrical and Electronics Engineers (IEEE), 2003, 12-25
Skup
Eurocon 2003
Mjesto i datum
Ljubljana, Slovenija, 22.09.2003. - 24.09.2003
Vrsta sudjelovanja
Predavanje
Vrsta recenzije
Međunarodna recenzija
Ključne riječi
formal verification ; model checking ; mutual exclusion algorithms ; CTL ; SMV
Sažetak
Mutual exclusion algorithms can exhibit intricate behavior for which correctness can be hard to establish. We demonstrate automatic verification of five algorithms by symbolic model checking. We used SMV tool which enables property specification in computation tree logic and allow us to impose fairness constraints on a model. For each of the algorithm we verify safety, liveness, non-blocking and no strict ordering properties.
Izvorni jezik
Engleski
Znanstvena područja
Računarstvo
POVEZANOST RADA
Projekti:
0098023
Ustanove:
Fakultet elektrotehnike i računarstva, Zagreb,
Institut "Ruđer Bošković", Zagreb
