Formal verification of distributed mutual-exclusion circuits - Meolic, Robert (Informacije MIDEM, 2003)
Vezja za porazdeljeno medsebojno izkljueevanje (DME) so zanimiv primer asinhronih vezij. Sestavljena so iz enakih celic DME, povezanih v obroe poljubne velikosti. Vsaka od celic DME ponuja prikljueno toeko za enega uporabnika in vsi uporabniki med seboj tekmujejo za izkljueen dostop do skupnega vira. V elanku obravnavamo formalno verifikacijo dveh znanih izvedb vezja DME. Obnašanje vezij opišemo s preprostim procesom, zahtevane lastnosti pa s temporalno logiko ACTL. Na ta naein smo lahko odkrili hazarde ter verificirali pravilnost obnašanja vezij v fundamentalnem naeinu delovanja.
Keywords: asinhrono vezje; digitalni sistemi; modeli; telecommunication; telekomunikacije; testiranje