Abstract Regelbunden modellkontroll är en generisk teknik för verifiering av oändligt tillstånd och/eller parametriserade system som använder finita ordautomata eller ändliga trädautomata för att finit representera potentiellt oändliga uppsättningar av tillgängliga konfigurationer av de system som verifieras. De problem som tas upp genom regelbunden modellkontroll är vanligtvis obeslutbara. För att underlätta terminering i så många fall som möjligt krävs acceleration vid inkrementell beräkning av uppsättningen tillgängliga konfigurationer vid regelbunden modellkontroll. I detta arbete beskriver vi hur olika stegvis refinerbara abstraktioner på ändliga (ord och träd) automata kan användas för detta ändamål. Dessutom ökar användningen av abstraktion inte bara möjligheterna för tekniken att upphöra, utan minskar också avsevärt problemet med en explosion i antalet tillstånd i automaten som genereras av regelbunden modellkontroll. Vi illustrerar effektiviteten i abstrakt regelbunden (träd) modell kontroll i verifiering av enkla system med olika källor av oändlighet såsom obundna räknare, köer, stackar och parametrar. Vi visar sedan hur abstrakt regelbunden trädmodellkontroll kan användas för verifiering av program som manipulerar trädliknande dynamiska datastrukturer. Ännu mer komplexa datastrukturer kan hanteras med hjälp av en lämplig trädliknande kodning.
I REF, Bouajjani et al. föreslå en verifieringsmetod baserad på abstractions och trädgivare applikationer på trädautomata språk, kallas Abstract Regular Tree Model Checking.
Abstract regular (tree) model checking
{'venue': 'International Journal on Software Tools for Technology Transfer', 'journal': 'International Journal on Software Tools for Technology Transfer', 'mag_field_of_study': ['Computer Science']}