Abstrakt. En av de främsta fördelarna med modellkontroll är framställning av motexempel som visar att ett system inte uppfyller en specifikation. Det kan dock kräva en hel del mänsklig ansträngning för att extrahera kärnan i ett fel från även en detaljerad källa-nivå spår av en misslyckad körning. Vi använder en automatiserad metod för att hitta flera versioner av ett fel (och liknande utföranden som inte producerar ett fel), och analysera dessa utföranden för att producera en mer kortfattad beskrivning av de viktigaste delarna av felet. Beskrivningen omfattar identifiering av delar av källkoden som är avgörande för att skilja mellan misslyckade och efterföljande körningar, skillnader i variation mellan misslyckade och icke-falska körningar och information om nödvändiga ändringar i schemaläggning och miljöåtgärder som krävs för att få framgångsrika körningar att misslyckas.
I REF föreslår författarna automatiserade metoder för analys av variationer i ett motexempel, för att identifiera delar av källkoden som är avgörande för att skilja fel och lyckade körningar.
What Went Wrong: Explaining Counterexamples
{'venue': 'In SPIN Workshop on Model Checking of Software', 'journal': None, 'mag_field_of_study': ['Computer Science']}