SAMMANFATTNING Bevis skrivna på algebraiska specifikationsspråk kallas bevispoäng. Proof score-metoden för konstruktionskontroll är attraktiv eftersom den ger ett flexibelt sätt att bevisa att konstruktioner för system uppfyller egenskaper. Hittills har dock strategin inriktats på säkerhetsegenskaper. I detta dokument beskriver vi ett sätt att verifiera att konstruktioner för system uppfyller levande egenskaper med tillvägagångssättet. Ett protokoll om ömsesidig uteslutning som använder en kö används som exempel. Vi beskriver designverifieringen och förklarar hur det verifieras att protokollet uppfyller lockoutfriheten.
2 senare i detta dokument) beskrivs i REF.
Proof Score Approach to Verification of Liveness Properties
{'venue': 'IEICE Transactions', 'journal': 'IEICE Transactions', 'mag_field_of_study': ['Computer Science']}