ВЕРИФИКА́ЦИЯ

ВЕРИФИКА́ЦИЯ в ин­фор­ма­ти­ке, про­цесс оп­ре­де­ле­ния то­го, удов­ле­тво­ря­ют ли ре­зуль­та­ты те­ку­ще­го эта­па раз­ра­бот­ки объ­ек­та (напр., про­грамм­но-ап­па­рат­ной сис­те­мы) тре­бо­ва­ни­ям, ус­та­нов­лен­ным для них на пре­ды­ду­щем эта­пе; про­цесс про­вер­ки вы­пол­не­ния за­дан­ных свойств объ­ек­та. В. на­зы­ва­ют и лю­бые дей­ст­вия, вы­пол­няе­мые в хо­де это­го про­цес­са.

Про­ве­ряе­мый в хо­де В. объ­ект час­то на­зы­ва­ют реа­ли­за­ци­ей, а про­ве­ряе­мые свой­ст­ва – спе­ци­фи­ка­ци­ей. В. мо­жет от­но­сить­ся к про­грамм­но­му или ап­па­рат­но­му обес­пе­че­нию, а так­же к про­грамм­но-ап­па­рат­но­му ком­плек­су в це­лом. В. бы­ва­ет ста­ти­че­ской и ди­на­ми­че­ской в за­ви­си­мо­сти от то­го, про­во­дит­ся ли она без функ­цио­ни­ро­ва­ния про­ве­ряе­мой реа­ли­за­ции (мо­де­ли) или в хо­де её ра­бо­ты.

В. мо­жет осу­ще­ст­в­лять­ся пу­тём по­строе­ния фор­маль­но­го до­ка­за­тель­ст­ва (или оп­ро­вер­же­ния) со­от­вет­ст­вия реа­ли­за­ции спе­ци­фи­ка­ци­ям. В этом слу­чае го­во­рят о фор­маль­ной ве­ри­фи­ка­ции. Фор­маль­ная ста­тич. В. воз­мож­на, ко­гда фор­маль­но оп­ре­де­ле­ны про­ве­ряе­мые свой­ст­ва и мо­дель, пред­став­ляю­щая реа­ли­за­цию. Напр., про­ве­ряе­мым свой­ст­вом мо­жет быть на­сту­п­ле­ние к.-л. со­бы­тия при оп­ре­де­лён­ных ус­ло­ви­ях в рам­ках ко­неч­но­го ав­то­ма­та, опи­сы­ваю­ще­го реа­ли­за­цию. Сре­ди ме­то­дов фор­маль­ной ста­тич. В. вы­де­ля­ют ана­ли­ти­че­скую В., с по­мо­щью ко­то­рой про­ве­ряе­мые свой­ст­ва до­ка­зы­ва­ют­ся или оп­ро­вер­га­ют­ся на ос­но­ве к.-л. ло­гич. ис­чис­ле­ния, и ме­тод про­вер­ки на мо­де­лях (model checking), сво­дя­щий ис­сле­до­ва­ние этих свойств к про­вер­ке их на ко­неч­ном мно­же­ст­ве со­стоя­ний реа­ли­за­ции.

Не­фор­маль­ная ста­тич. В. сво­дит­ся к со­вме­ст­но­му ана­ли­зу до­ку­мен­тов, ко­да про­грамм, мо­де­лей или схем, пред­став­ляю­щих спе­ци­фи­ка­цию и реа­ли­за­цию. Напр., од­ним из та­ких под­хо­дов яв­ля­ет­ся ин­спек­ция про­грамм.

Ос­нов­ной и наи­бо­лее ши­ро­ко при­ме­няе­мый вид ди­на­мич. В. – тес­ти­ро­ва­ние. Фор­маль­ное тес­ти­ро­ва­ние ос­но­вы­ва­ет­ся на не­ко­то­рых ги­по­те­зах о реа­ли­за­ции и, ис­хо­дя из них и фак­тич. ре­зуль­та­тов функ­цио­ни­ро­ва­ния реа­ли­за­ции, до­ка­зы­ва­ет или оп­ро­вер­га­ет её со­от­вет­ст­вие спе­ци­фи­ка­ции. Разл. ви­ды фор­маль­ных мо­де­лей и ис­чис­ле­ний, ис­поль­зуе­мые для фор­маль­ной В., мо­гут быть клас­си­фи­ци­ро­ва­ны сле­дую­щим об­ра­зом: ис­пол­няе­мые мо­де­ли (ав­то­ма­ты и их разл. рас­ши­ре­ния, сис­те­мы пе­ре­хо­дов и их рас­ши­ре­ния, сис­те­мы взаи­мо­дей­ст­вую­щих ав­то­ма­тов или сис­те­мы пе­ре­хо­дов, се­ти Пет­ри); ло­гич. и ал­геб­ра­ич. ис­чис­ле­ния (ло­ги­ка Хоа­ра и кон­тракт­ные мо­де­ли, ал­геб­ра­ич. опи­са­ния аб­ст­ракт­ных ти­пов дан­ных, вре­мен­ные ло­ги­ки, ре­ля­ци­он­ные ал­геб­ры); про­ме­жу­точ­ные мо­де­ли (ал­геб­ры про­цес­сов, ма­ши­ны с аб­ст­ракт­ны­ми со­стоя­ния­ми, лам­бда-ис­чис­ле­ние и его рас­ши­ре­ния).

Для боль­шин­ст­ва раз­ра­бот­чи­ков ис­пол­ни­мые мо­де­ли бо­лее по­нят­ны и удоб­ны в при­ме­не­нии, чем ло­ги­ко-ал­геб­раи­че­ские. Од­на­ко они тре­бу­ют бо­лее де­таль­ной про­ра­бот­ки и по­это­му ча­ще ис­поль­зу­ют­ся для пред­став­ле­ния реа­ли­за­ции, а ло­ги­ко-ал­геб­ра­ич. мо­де­ли ча­ще при­ме­ня­ют­ся для пред­став­ле­ния спе­ци­фи­ка­ции. В ря­де слу­ча­ев и спе­ци­фи­ка­ция, и реа­ли­за­ция пред­став­ле­ны в ви­де ис­пол­ни­мых мо­де­лей или мо­де­лей про­ме­жу­точ­но­го ти­па.