Validarea modelului

Versiunea actuală a paginii nu a fost încă examinată de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită pe 26 august 2019; verificările necesită 2 modificări .

Verificarea modelului ( verificarea modelului , verificarea modelului în engleză ) este o metodă de verificare formală automată a sistemelor paralele cu un număr finit de stări, vă permite să verificați dacă un anumit model de sistem satisface specificațiile formale.

Așa -numitul model Kripke este de obicei folosit ca model , care este definit formal după cum urmează: , unde este setul de stări, este setul de stări inițiale, este raportul de tranziție, este funcția de etichetare. $M = \stânga(S, S_0, R, L\dreapta)$ $S$ $S_{0}$ $R \subseteq S \times S$ $L: S \rightarrow 2^{AP}$

De obicei, specificațiile sunt date în limbajul logicii formale. Pentru specificarea hardware-ului și software-ului, de regulă, se utilizează logica temporală - un limbaj special care vă permite să descrieți comportamentul sistemului în timp.

O problemă importantă de specificație este completitudinea. Metoda de verificare a modelului face posibilă verificarea faptului că modelul sistemului proiectat corespunde unei specificații date, cu toate acestea, este imposibil să se determine dacă specificația dată acoperă toate proprietățile pe care sistemul trebuie să le satisfacă.

Principala dificultate care trebuie depășită în timpul testării pe modele este legată de efectul de explozie combinatorie în spațiul de stare. Această problemă apare în sistemele cu multe componente care interacționează între ele, precum și în sistemele cu structuri de date care pot lua un număr mare de valori.

Instrumente

BLAST - analizor static de programe C
CADP (Construction and Analysis of Distributed Processes) este un instrument de proiectare pentru protocoale și sisteme distribuite
CHESS este un instrument de testare a programelor multi-threaded pentru .Net ( administrat ) și Win32, 64
ISP - Verificator de cod de program MPI
Java Pathfinder este un instrument gratuit pentru verificarea programelor Java cu mai multe fire.
MoonWalker este un instrument gratuit pentru testarea programelor .Net
MRMC (Markov Reward Model Checker)
NuSMV - verificator simbolic
PRISM - verificator simbolic probabilist
Rabbit - verificator pentru sisteme în timp real
SPIN este un verificator de uz general pentru verificarea corectitudinii programelor și protocoalelor distribuite
Vereofy - verificator de programe de sisteme componente
μCRL2 este un instrument gratuit bazat pe ACP
UPPAAL este un set de instrumente pentru modelarea, verificarea și validarea sistemelor în timp real modelate ca rețele de automate temporale
Zing [1] este un set de instrumente de dezvoltare a driverelor Microsoft care vă permite să verificați modelele de stare ale software-ului simultan .

Note

↑ Zing . Preluat la 18 iulie 2018. Arhivat din original la 18 iulie 2018. (nedefinit)

Literatură

Clark E. M., Gramberg O., Peled D. Verificarea modelelor de programe. Verificarea modelului. - M. : MTSNMO, 2002. - 416 p. — ISBN 5940570542 .
Karpov Yu. G. Verificare model. Verificarea sistemelor software paralele și distribuite. - Sankt Petersburg. : BHV-Petersburg, 2009. - 460 p. — ISBN 9785977504041 .
Velder S. E., Lukin M. A., Shalyto A. A., Yaminov B. R. Verificarea programelor automate. - Universitatea de Stat din Sankt Petersburg ITMO, 2011. - 242 p.

Link -uri

Verificarea programelor folosind modele // Open Systems, Nr. 12, 2003
Robert B. Franţa Modelarea şi Analiza Sistemelor Concurente
Mironov A. M. Verificarea programelor prin metoda Model Checking.