Abstrakt. I detta dokument beskriver vi en helt automatiserad ram för iterativ abstraktion förfining som är helt integrerad i en formell-verifiering miljö. Denna miljö består av tre grundläggande programvaruverktyg: Prognos, en BDD-baserad modellkontroll, Thunder, en SAT-baserad begränsad modellkontroll, och MCE, en teknik för multi-counterexempel analys. I vårt ramverk väljs den initiala abstraktionen i förhållande till den egendom som är under kontroll. Abstractionen är modellkontrollerad av Forecast; vid fel returneras ett motexempel. Vårt ramverk innehåller en abstrakt motexempelanalysatormodul som tillämpar tekniker för begränsad modellkontroll för att kontrollera om det abstrakta motexempelet håller i betongmodellen. Om den gör det utsträcks den till ett konkret motexempel. Denna viktiga förmåga tillhandahålls som ett separat verktyg som också tar upp ett av de största problemen med verifiering genom manuell abstraktion. Om motexempelet är falskt, använder vi en ny förfining heuristic baserad på MCE för att vägleda förfiningen. Efter att den del av den abstrakta modellen som ska förfinas har valts, beräknar vår förfiningsalgoritm en ny abstraktion som inkluderar så mycket logik som möjligt utan att lägga till för många nya variabler, vilket skapar en balans mellan att förfina abstraktionen och hålla dess storlek hanterbar. Vi visar effektiviteten i vårt ramverk på utmanande Intel konstruktioner som inte var tillgängliga för BDD-baserade modell-kontroll metoder.
I REF används en modellkontroll iterativt för att förfina en abstrakt modell.
Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation
{'venue': 'TACAS', 'journal': None, 'mag_field_of_study': ['Computer Science']}