Modellvalidering

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 26 augusti 2019; kontroller kräver 2 redigeringar .

Modellkontroll ( model checking , engelska  model checking ) är en metod för automatisk formell verifiering av parallella system med ett ändligt antal tillstånd, den låter dig kontrollera om en given systemmodell uppfyller formella specifikationer.

Den så kallade Kripke - modellen används vanligtvis som modell , som formellt definieras enligt följande: , där  är mängden tillstånd,  är mängden initiala tillstånd,  är övergångsförhållandet,  är märkningsfunktionen.

Vanligtvis ges specifikationer på den formella logikens språk. För specifikationen av hårdvara och mjukvara används som regel tidslogik  - ett speciellt språk som låter dig beskriva systemets beteende i tid.

En viktig specifikationsfråga är fullständighet. Modellkontrollmetoden gör det möjligt att verifiera att modellen av det system som konstrueras motsvarar en given specifikation, dock är det omöjligt att avgöra om den givna specifikationen omfattar alla egenskaper som systemet måste uppfylla.

Den största svårigheten som måste övervinnas under testning av modeller är relaterad till den kombinatoriska explosionseffekten i tillståndsrummet. Detta problem uppstår i system med många komponenter som interagerar med varandra, såväl som i system med datastrukturer som kan anta ett stort antal värden.

Verktyg

Anteckningar

  1. ↑ Zing . Hämtad 18 juli 2018. Arkiverad från originalet 18 juli 2018.

Litteratur

Länkar