Ариан-5 Верификация – белгіленген талаптардың орындалғаны туралы объективті куәліктерді ұсыну негізінде растау

Верификация – белгіленген талаптардың орындалғаны туралы объективті куәліктерді ұсыну негізінде растау.

Верификация (лат. verus-дұрыс) – бұл өнім тұжырымдалған талаптарды қанағаттандырады.

Валидация – нақты пайдалануға немесе қолдануға арналған талаптардың орындалғаны туралы объективті куәліктерді ұсыну негізінде растау.

Валидация – нақты пайдалануға немесе қолдануға арналған талаптардың орындалғаны туралы объективті куәліктерді ұсыну негізінде растау.

Валидация (лат. validus-сау) – бұл тапсырыс беруші талап еткен нәрсенің орындалғанын тексеру. Әдетте әзірленген жүйені тестілеу және модельдеу валидация бөлігі ретінде қарастырылады.

Бағдарламаларды формальды верификациялау – бұл бағдарламалық жүйенің моделі берілген формальды ерекшелікті қанағаттандыратын формальды дәлелдеудің (немесе теріске шығарудың) тәсілдері мен әдістері.

Бағдарламаларды формальды верификациялау – бұл бағдарламалық жүйенің моделі берілген формальды ерекшелікті қанағаттандыратын формальды дәлелдеудің (немесе теріске шығарудың) тәсілдері мен әдістері.

Верификацияны орындау үшін бағдарламаның спецификациясы жүйе мінез-құлқының қалаулы қасиеттері туралы формальды тұжырымдар жиынтығынан тұруы тиіс. Формальды ерекшелік үшін логика тілі қолданылады, оның әрбір бекітуі тексерілетін бағдарламалық жүйе үшін шынайы немесе жалған болуы мүмкін. Верификатор берілген формальды модельде берілген формальды бекітулердің орындалуын тексереді.

Верификацияны орындау үшін бағдарламаның спецификациясы жүйе мінез-құлқының қалаулы қасиеттері туралы формальды тұжырымдар жиынтығынан тұруы тиіс. Формальды ерекшелік үшін логика тілі қолданылады, оның әрбір бекітуі тексерілетін бағдарламалық жүйе үшін шынайы немесе жалған болуы мүмкін. Верификатор берілген формальды модельде берілген формальды бекітулердің орындалуын тексереді.

дедуктивтік верификация;

• дедуктивтік верификация;
• Баламалылығын тексеру;
• model checking (модельді тексеру).

Дедуктивтік верификация-бұл дұрыс логикалық жүйедегі теоремаларды дәлелдеуге түсетін бағдарламаның дұрыстығын тексеру. Бұл бағыт Роберт Флойд пен Энтони Хоар алғаш рет бағдарламалардың дұрыстығын дәлелдеу проблемасын ресми түрде қойып отырғаннан бері 40 жылдан астам уақыт бойы әзірленуде. Бұл жерде бағдарламаларды верификациялау аксиом және шығару ережелері негізінде дедукциямен жүргізіледі. Бұл өте күрделі рәсім толығымен автоматтандырылуы мүмкін емес, ол инварианттарды құру және балама емес таңдау кезінде интуицияны пайдаланатын болжамдар негізінде әрекет ететін адамның қатысуын талап етеді.

Дедуктивтік верификация-бұл дұрыс логикалық жүйедегі теоремаларды дәлелдеуге түсетін бағдарламаның дұрыстығын тексеру. Бұл бағыт Роберт Флойд пен Энтони Хоар алғаш рет бағдарламалардың дұрыстығын дәлелдеу проблемасын ресми түрде қойып отырғаннан бері 40 жылдан астам уақыт бойы әзірленуде. Бұл жерде бағдарламаларды верификациялау аксиом және шығару ережелері негізінде дедукциямен жүргізіледі. Бұл өте күрделі рәсім толығымен автоматтандырылуы мүмкін емес, ол инварианттарды құру және балама емес таңдау кезінде интуицияны пайдаланатын болжамдар негізінде әрекет ететін адамның қатысуын талап етеді.

Баламалылықты тексеру өзара іс-қимыл жасайтын үдерістердің формальды модельдерін әзірлеумен, осындай модельдер шеңберінде спецификацияны да, іске асыруды да білдірумен және мінез-құлықтың формальды белгілі бір модельдерінің мінез-құлқының баламалығын тексерумен байланысты. Бұл бағыт Робин Милнердің жұмысы 30 жыл бұрын өзара әрекет ететін жүйелерді есептеу (Calculus of Communicating Systems, CCS) үдерістерінің Алгебрасын әзірлеумен басталды.

Баламалылықты тексеру өзара іс-қимыл жасайтын үдерістердің формальды модельдерін әзірлеумен, осындай модельдер шеңберінде спецификацияны да, іске асыруды да білдірумен және мінез-құлықтың формальды белгілі бір модельдерінің мінез-құлқының баламалығын тексерумен байланысты. Бұл бағыт Робин Милнердің жұмысы 30 жыл бұрын өзара әрекет ететін жүйелерді есептеу (Calculus of Communicating Systems, CCS) үдерістерінің Алгебрасын әзірлеумен басталды.

Model checking (модельді тексеру) – бұл жүйенің осы формальды моделінде берілген логикалық формула (шынайы мәнді қабылдайды) орындалғанын тексеру әдісі. Бұл әдіс 20 жылдан астам дамыды. Model checking әдісі толығымен автоматтандырылуы мүмкін.

Model checking (модельді тексеру) – бұл жүйенің осы формальды моделінде берілген логикалық формула (шынайы мәнді қабылдайды) орындалғанын тексеру әдісі. Бұл әдіс 20 жылдан астам дамыды. Model checking әдісі толығымен автоматтандырылуы мүмкін.

Model checking —бұл берілген Ф логикалық формуласы М өтудің осы жүйесі үшін шынайы бола ма, яғни М модель Ф.

Model checking —бұл берілген Ф логикалық формуласы М өтудің осы жүйесі үшін шынайы бола ма, яғни М модель Ф.

жүктеу/скачать 1,07 Mb.

Достарыңызбен бөлісу: