Modellkontroll

Modellkontroll är en formell verifikationsmetod som används för att automatiskt avgöra om en modell av ett beräkningssystem uppfyller angivna krav. En modell består vanligtvis av ett antal tillstånd och övergångar mellan dem, medan kraven ofta formuleras i temporala logiker som CTL eller LTL.

Principen är att systematiskt utforska hela tillståndsrymden (eller en relevant del där det är möjligt) och avgöra om kraven är uppfyllda. Om en egenskap inte uppfylls genereras oftast ett motexempel som illustrerar i vilket tillstånd och vilken övergång felet uppstår.

Metoderna varierar mellan explicit-state modellkontroll, där varje tillstånd behandlas individuellt, och symbolisk modellkontroll, som använder BDD:er eller SAT/SMT-lösare för att effektivt representera stora utrymmen. För att hantera state explosion används tekniker som partial-order reduction, abstraktion och CEGAR (Counterexample-Guided Abstraction Refinement).

Användningsområden inkluderar hårdvaruverifikation, kommunikationsprotokoll, realtidssystem och multitrådade program. Det finns även probabilistisk modellkontroll som hanterar osäkerhet och slumpmässiga beteenden i system, till exempel med Markov-kedjor och verktyg som PRISM.

Historiskt utvecklades modellkontroll i början av 1980-talet av forskare som E. Clarke och E. Allen Emerson. Sedan dess har tekniken utökats med större fokus på skalbarhet, verktygsstöd och integration i utvecklingsprocesser.

Se även: CTL, LTL, formell verifiering, modellbaserad design, TLA+.