ABSTRACT Vi presenterar en begränsningsorienterad statsbaserad bevismetod för samtidiga programvarusystem som utnyttjar kompositionalitet och abstraktion för att minska verikationsproblemet under utredning. Formell grund för denna metod är Modal Transition Systems som tillåter lös state-baserade specificationer, som kan ändras genom successiva tillägg av begränsningar. Nyckelbegrepp i vår metod är projektiva vyer, åtskillnad av bevisskyldigheter, Skolemization och abstraktion. Centralt till metoden är användningen av Parametrized Modal Transition Systems. Metoden överförs enkelt till realtidssystem, där det största problemet är parametrar för tidsbegränsningar.
Larsen m.fl. använda projektiva synpunkter för en begränsad, bevisbaserad metod för trafikomställningssystem REF.
A Constraint Oriented Proof Methodology Based on Modal Transition Systems
{'venue': 'TACAS', 'journal': None, 'mag_field_of_study': ['Computer Science']}