Modelvalidering

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 26. august 2019; checks kræver 2 redigeringer .

Modelkontrol ( model checking , engelsk  model checking ) er en metode til automatisk formel verifikation af parallelle systemer med et begrænset antal tilstande, det giver dig mulighed for at kontrollere om en given systemmodel opfylder formelle specifikationer.

Den såkaldte Kripke - model bruges normalt som model , som formelt defineres som følger: , hvor  er mængden af ​​tilstande,  er mængden af ​​begyndelsestilstande,  er overgangsforholdet,  er mærkningsfunktionen.

Normalt er specifikationer givet i den formelle logiks sprog. Til specifikation af hardware og software bruges som regel tidsmæssig logik  - et specielt sprog, der giver dig mulighed for at beskrive systemets adfærd i tide.

Et vigtigt specifikationsspørgsmål er fuldstændighed. Modeltjekmetoden gør det muligt at verificere, at modellen af ​​det system, der designes, svarer til en given specifikation, dog er det umuligt at afgøre, om den givne specifikation dækker alle de egenskaber, som systemet skal opfylde.

Den største vanskelighed, der skal overvindes i løbet af afprøvning på modeller, er relateret til den kombinatoriske eksplosionseffekt i tilstandsrummet. Dette problem opstår i systemer med mange komponenter, der interagerer med hinanden, såvel som i systemer med datastrukturer, der kan antage et stort antal værdier.

Værktøjer

Noter

  1. ↑ Zing . Hentet 18. juli 2018. Arkiveret fra originalen 18. juli 2018.

Litteratur

Links