Rasmiy (ekvivalentlikni tekshirish, modelni tekshirish, deduktiv tahlil) va norasmiy (imtihon, sinov) tekshirish usullari mavjud

O`ZBEKISTON RESPUBLIKASI AXBOROT TEXNOLOGIYALARI VA KOMMUNIKATSIYALARINI RIVOJLANTIRISH VAZIRLIGI
MUHAMMAD AL-XORAZMIY NOMIDAGI
TOSHKENT AXBOROT TEXNOLOGIYALARI
UNIVERSITETI SAMARQAND FILIALI

"Kompyuter injiniring" fakulteti

"Kampyuter tizimlar" kafedrasi
"Dastur tekshirish farmal usullari ” fanidan
1-Mustaqil ish
Mavzu: Ketma-ket dasturlarni deduktiv tekshirish


Bajardi :Ki103-19-gurux
Azizbek A
Tekshirdi : Maxmudov R
Samarqand -2023
Mavzu: Ketma-ket dasturlarni deduktiv tekshirish
Reja:
1. Dasturlardagi xatolar
2. Dasturlar formal usullari
3. Ketma-ket dasturlarni deduktiv tekshirish
1. Dasturlardagi xatolar.
Rasmiy (ekvivalentlikni tekshirish, modelni tekshirish, deduktiv tahlil) va norasmiy (imtihon, sinov) tekshirish usullari mavjud. Rasmiy tekshirishning umumiy sxemasi quyidagicha hisoblanadi:
• dastur dasturning rasmiy modeli, talablar - talablarning rasmiy modeli bilan moslashtirilgan;
• dasturning to'g'riligini tekshirish birinchi va ikkinchi modellar o'rtasida yozishmalarni o'rnatadigan rasmiy protseduraga qadar kamayadi.
Har qanday dasturda (hatto ehtiyotkorlik bilan disk raskadrovka qilingan dasturda) kamida bitta xato mavjud. Bu hazil, boshqa har qanday narsa singari, bexosdan paydo bo'lmagan: kompyuter tizimlarining juda murakkabligi (milliardlab tranzistorlar va millionlab kod satrlari) bilan xatolardan qochish mumkin emas - tizim talablarga mos kelmaydi - bu mumkin emas. E'tibor bering, biz nafaqat har doim ham vakolatli mutaxassislar tomonidan shoshilinch ravishda ishlab chiqilgan amaliy "dasturiy ta'minot" haqida emas, balki mas'uliyatli tarkibiy qismlar, shu jumladan apparat (mikroprotsessorlar, kirish-chiqarish moslamalari) va tizim dasturlari (operatsion tizimlar, kompilyatorlar) haqida ham gaplashamiz.
Loyihalash va amalga oshirishda xatolarga yo'l qo'yilgan tizimlar ma'lum vaziyatda o'zlarini oldindan aytib bo'lmaydigan darajada tutishi va jiddiy oqibatlarga olib kelishi mumkinligi aniq. Mana ulardan ba'zilari.
1. 1982 yilda Kanadaning Atomic Energy of Canada Limited kompaniyasi radiatsiya terapiyasi - saraton kasalligini nurlantirish uchun mo'ljallangan "Therac-25" tibbiyot turkumini ishga tushirdi. "Kamdan-kam" holatlarda, o'rnatilgan boshqaruv tizimini loyihalash va amalga oshirishda bir qator xatolar tufayli nurlanish intensivligi 2 daraja yoki undan yuqori darajaga oshdi. Qurilmaning ishlashi paytida (1985 yil iyunidan 1987 yil yanvarigacha bo'lgan davr) kamida ikkita bemor vafot etdi, bir nechta odam nogiron bo'lib qoldi.
2. 1988 yil 2 sentyabrda Mars va uning sun'iy yo'ldoshi Fobosni o'rganish uchun 7 iyulda boshlangan Sovet sayyoralararo "Fobos1" stantsiyasi bilan aloqa uzildi. 29-avgust kuni Yerdan noto'g'ri buyruq uzatildi, uni samolyot bortidagi tizim noto'g'ri yo'naltirish va barqarorlashtirish tizimini o'chirish buyrug'i sifatida qabul qildi. Stansiya quyosh panellarini Quyoshga yo'naltirishni to'xtatdi, natijada uning batareyalari tugadi. Olti oy o'tib, "Fobos-2", zaxira nusxasi "Fobos-1" bilan aloqa uzildi. Ikkala missiyaning asosiy vazifasi - uzoq umr ko'rgan avtonom stantsiyani Fobos yuzasiga etkazish - bajarilmay qoldi
3. 1994 yil 13-iyun kuni Intel Pentium mikroprotsessorida suzuvchi nuqta raqamlarini ajratish bo'yicha yo'riqnomani amalga oshirishda xato aniqlandi (bo'linish birligining dastlabki taxminlar jadvalida bir nechta noto'g'ri qiymatlar mavjud edi). Va shaxsiy kompyuterlarning oddiy foydalanuvchilari, o'z qiyofasini saqlab qolish uchun kompaniyani bezovta qilmasliklari kerak edi, ammo ular chiqarilgan mikrosxemalarni bepul almashtirishlari kerak edi. Buning qiymati 475 million dollarni tashkil etdi.
4. 1996 yil 4 iyunda, uchirilgandan 39 soniyada, Evropa kosmik agentligi tomonidan ishlab chiqilgan Ariane 5 raketasi portladi. Bortdagi tizim qisman raketaning oldingi versiyasi "Ariane 4" ning dasturiy ta'minotidan, xususan inertial navigatsiya tizimini boshqarish modulidan qisman foydalangan. Raketaning burilishini bildiruvchi 64-bitli suzuvchi nuqta raqamidan modul tomonidan ishlov berilmagan 16-bitli butun songa aylantirish paytida toshma yuz berdi. Modulni ishlab chiqish paytida raketaning jismoniy cheklovlari tufayli toshib ketish mumkin emas deb taxmin qilingan edi, ammo taraqqiyot, siz bilganingizdek, bir joyda turmaydi - Arian 5-da yangi dvigatellar ishlatilgan.
5. 2003 yil 23 martda Iroqdagi urush paytida Amerikaning Patriot zenit-raketa tizimi Kuvayt chegarasi yaqinida uchib yurgan Britaniyaning Tornado bombardimonchi samolyotini dushman raketasi deb xato qilib aniqladi va avtomatik ravishda o'q uzdi. Ikki uchuvchi halok bo'ldi. Bir yarim hafta o'tgach, 2 aprel kuni "do'stona olov" Amerika aviatashuvchisiga asoslangan F / A-18 "Hornet" qiruvchi-bombardimonchi samolyotini yo'q qildi. Yana bir uchuvchi halok bo'ldi.
Kompyuter tizimlaridagi xatolar istisno emasligini tushunish muhimdir. Statistik ma'lumotlarga ko'ra, o'rnatilmagan kodning ming satriga to'g'ri keladigan xatolar soni o'rtacha 10-505 gacha. Bundan tashqari, dizayn sifatini pasayish tendentsiyasi mavjud (ehtimol bu tizimlarning murakkabligi va ularni yaratish xarajatlarini optimallashtirishning natijasidir): "Chalkashtirish va buzish qobiliyati nuqtai nazaridan kompyuter har kuni tobora ko'proq odamga o'xshaydi. " Shu bilan birga, bizning hayotimiz tobora kompyuterlarga bog'liq bo'lib qolmoqda, shuning uchun kompyuter tizimlarining to'g'riligi va ishonchliligini ta'minlash (boshqacha qilib aytganda, tekshirish) tobora muhim ahamiyat kasb etmoqda.
2. Dasturlar formal usullari
Rasmiy tekshirish dasturlarni matematik (mantiqiy) modellashtirish va ularning talablariga asoslanadi. Bu erda g'oyalar bilimlarning boshqa sohalarida modellardan foydalanishda aynan bir xil: model yaratiladi - o'rganilayotgan ob'ekt yoki hodisaning idealizatsiyalangan tavsifi; model matematik usullar yordamida o'rganiladi; tadqiqot natijalari haqiqiy ob'ekt yoki hodisaga o'tkaziladi. Albatta, ushbu yondashuvning qo'llanilishi ishlatilgan modellar bilan belgilanadi - ularning etarliligi shartlarini aniq tushunishingiz kerak.

Рисунок 1. Общая схема формальной верификации

Formal usulning umumiy sxemasi 1-rasm: dasturning rasmiy modeli yaratilgan; talablarning rasmiy modeli yaratiladi; dastur modelining talablar modeliga muvofiqligi rasmiy ravishda tekshiriladi; tekshirish natijalariga ko'ra haqiqiy dasturning haqiqiy talablarga muvofiqligi yoki mos kelmasligi to'g'risida (boshqacha aytganda, dasturda xatolarning yo'qligi yoki mavjudligi to'g'risida) xulosa qilinadi. Dastur modellari va talablari modellarini namoyish qilish uchun mos ravishda dasturlarning rasmiy spetsifikatsiyasi tillari (modellashtirish tillari) va talablarning rasmiy spetsifikatsiyasi tillari qo'llaniladi; bunday tillarning namunalari qo'llanmada muhokama qilinadi.

Formal usullari dastur modellari turlari (cheklangan avtomatlar, Petri tarmoqlari, belgilangan o'tish tizimlari), talablar modellari turlari (dasturiy ta'minot shartnomalari, ishlab chiqarish qoidalari, vaqtinchalik bayonotlar), yozishmalar munosabatlari (ekvivalentlik, simulyatsiya, izlarni kiritish) va muvofiqlik bilan farqlanadi. tekshirish texnikasi (kosmik holatlarni o'rganish, ramziy tahlil, deduktiv xulosa).
Quyida biz rasmiy tekshirish usullarining ekvivalentni tekshirish, modelni tekshirish va deduktiv tahlil kabi turlarini batafsil ko'rib chiqamiz.
Ekvivalentlikni tekshirish. Ekvivalentlikni tekshirishda dastur modeli va talablar modeli bir xil (masalan, har ikkala model ham cheklangan avtomat, yoki har ikkala model ham Turing mashinalari) va ko'rib chiqilayotgan turdagi modellar uchun belgilangan ekvivalentlik munosabatlaridan biri yozishma munosabati sifatida ishlatiladi. Bajariladigan modellarning (avtomatlar, dasturlar va boshqalar) ekvivalentligini tekshirishda talablar modeli mos yozuvlar modeli yoki mos yozuvlar dasturlari deb nomlanadi.
Kirish va chiqish o'zgaruvchilari bir xil bo'lgan ikkita (deterministik) ketma-ket dasturlar, agar ularning domenlari bir-biriga to'g'ri keladigan bo'lsa (funktsional) ekvivalent deb aytiladi (bitta dastur uchun tegishli bo'lgan har qanday kirish ma'lumoti boshqasiga tegishli bo'lsa) va har qanday tegishli kirish ma'lumotlari uchun ular bir xil qaytaradilar natijalar ...
1.2-misol. Quyidagi 1.1-jadvalda ikkita Evklid1 va Evklid2 dasturlari keltirilgan, ularning har biri x va y ning ikkita kirish tamsayı o'zgaruvchilariga ega, x> 0 va y> 0 va bitta chiqish tamsayı o'zgaruvchisi GCD:
Evklid algoritmining ikkita tatbiqi

// Evklid1.cpp : #include using namespace std; int main() { int x =120; int y = 18; cout <<"x= "<< x <<" y=" << y < while (x!= y) { if (x > y) x = x - y; else y = y - x; } cout <<"NOD="<< x << endl; return 0; }

// Evklid2.cpp : #include using namespace std; int main() { int x = 120; int y = 18; int z; cout << "x= " << x << " y=" << y << endl; while (y != 0) { z = x; x = y; y = z % y; } cout << "NOD=" << x << endl; return 0; }

Evklid1 va Evklid2 dasturlarining ekvivalentligini ko'rish juda oson - ikkalasi ham ikkita tabiiy sonning eng katta umumiy bo'luvchisini (GCD) hisoblashadi (bu Evklid algoritmining turli xil dasturlari). Ularning ekvivalentligini qanday rasmiy ravishda isbotlash mumkin?

Matematik jihatdan x = c * n, y = c * m va boshqalarni isbotlash mumkin
Biroq, avtomatik tekshirish haqida gapiradigan bo'lsak, kompyuter qanday qilib dastur nima bilan shug'ullanishini, uning "ma'nosi" ni qanday qilib "tushunishi" kerakligi aniq emas.
Siz boshqa yo'ldan borishingiz mumkin - taqqoslangan dasturlarning ma'nosini o'rganmasdan, ekvivalent o'zgarishlarni qo'llagan holda, boshqasiga (yoki har birining uchdan biriga) o'zgartirishga harakat qiling.
Ketma-ket dasturlar, yani alg'oritmlar, deduktiv tekshirishni amalga oshirish uchun quyidagi usullardan foydalanish mumkin:
Test qilish: Ketma-ket dasturni o'zgartirishsiz yoki kuchli testlar yordamida sinab ko'ring. Bu, dasturning asosiy funktsiyalarini va xususiyatlari tekshirilgan holda dasturda biron bir xatolik yoki nomutanosiblik borligini aniqlashga yordam beradi.
Kode analiz qilish: Ketma-ket dasturda kodning barcha qismlarini tekshirib, ushbu kodda xatolik yoki nomutanosibliklarni aniqlash mumkin. Bu, xususiyati dastur kichik bo'lsa va biron bir test qilish mumkin bo'lmagan vaqt uchun foydali bo'ladi.
Debug qilish: Debug oynasi yordamida ketma-ket dasturda sodir bo'lgan xatoliklarni topish va ularni tuzatish mumkin. Debug oynasida, dasturning har bir qadamini bajarishni to'xtatib, o'zini tekshirish va muammolarni aniqlash mumkin.
Kodni tiklash: Ketma-ket dasturda kodni to'g'rilash yordamida kodda xatolik yoki nomutanosibliklarini aniqlab, ularni tuzatish mumkin. Buni qilish uchun dasturning qayta yozilishini talab qilish kerak bo'ladi.
Formal verifikatsiya: Ketma-ket dasturda biron bir xatolik qolmaganini tasdiqlash uchun formal verifikatsiya yordamidan foydalanish mumkin. Bu usulda, dasturning ishlashini ko'rsatuvchi matematik modellari ishlatiladi.
Bu usullar ketma-ket dasturlarni deduktiv tekshirish uchun foydalaniladigan eng mashhur usullardir. Ushbu usullarning har biri biror xil natijalarga erishishga yordam beradi.
Deduktiv tekshirish, dasturlarning to'g'ri ishlashi uchun lozim bo'lgan shartlar va ehtimollar to'g'risida chora-tadbirlar amalga oshirish yordamida, dasturlarning xato yoki muammo qolmaganligini tasdiqlash usuli hisoblanadi.
Deduktiv tekshirishning boshqa ma'nolari ham mavjud, shu jumladan, matematik modellarda yoki tizimlarda muhim natijalarga erishishda foydalaniladigan ma'lumotlar yoki aniq xususiyatlarga asoslangan tasdiqlash usuli.
Bu usulda, dasturning to'g'ri ishlashi uchun kerakli bo'lgan barcha shartlar va ehtimollar aniqlanib, dastur yaratuvchisi tomonidan aniqlangan testlar yordamida, dastur to'g'ri ishlashi haqida aniqligi tasdiqlanadi.

Deduktiv tekshirishning muhim asosiy qismi, lozim bo'lgan shartlar va ehtimollar aniqlash va to'g'ri ishlash uchun testlar yaratishdir. Bu testlar odatda katta sonli ma'lumotlar to'plamidan tashkil topgan holda, dasturning barcha funktsiyalarini tekshirish uchun yaratiladi.

Deduktiv tekshirish, dasturlarning to'g'ri ishlashiga nisbatan yuzaga keladigan har qanday muammolarni aniqlashga yordam beradi va dasturni yaxshilash uchun zarur bo'lgan o'zgarishlarni belgilashga imkon beradi.

Deduktiv tekshirishda bir necha sinflarga bo'linadi, masalan, funksiyalar, klaslar, sinfdagi obyektlar va h.k. Shu sababli, quyidagi C++ kodida deduktiv tekshirishni ko'rsatishning yalpi darajasini ko'rsataman:
#include
using namespace std;

bool isEqual(int a, int b) {

if (a == b) {
return true;
} else {
return false;
}
}

int main() {

int x = 3;
int y = 4;
bool result;

result = isEqual(x, y);

if (result == true) {

cout << "x va y o'zaro teng." << endl;
} else {
cout << "x va y o'zaro teng emas." << endl;
}

return 0;

}
Deduktiv tekshirishda bir necha sinflarga bo'linadi, masalan, funksiyalar, klaslar, sinfdagi obyektlar va h.k. Shu sababli, quyidagi C++ kodida deduktiv tekshirishni ko'rsatishning yalpi darajasini ko'rsataman:

c
Copy code

#include
using namespace std;

bool isEqual(int a, int b) {

if (a == b) {
return true;
} else {
return false;
}
}

int main() {

int x = 3;
int y = 4;
bool result;

result = isEqual(x, y);

if (result == true) {

cout << "x va y o'zaro teng." << endl;
} else {
cout << "x va y o'zaro teng emas." << endl;
}

return 0;

}
Bu kodda, isEqual nomli bir funktsiya yaratilgan. Bu funktsiya ikkita butun sonni qabul qilib, ularning qiymatlari bir-biriga teng ekanligini aniqlaydi. Agar ikkisi bir-biriga teng bo'lsa, true qiymati qaytariladi; aks holda false qiymati qaytariladi.
Dasturda, x va y o'zgaruvchilariga mos qiymatlar ta'qdim etiladi. result o'zgaruvchisi isEqual funktsiyasini chaqiradi va isEqual funktsiyasidan qaytgan qiymatni saqlaydi.
So'nggi qadamda, result o'zgaruvchisining qiymati tekshiriladi. Agar true qiymati qaytgan bo'lsa, x va y o'zaro teng ekanligini tasdiqlash uchun cout operatori yordamida ma'lumot konsolga chiqariladi. Aks holda, x va y o'zaro teng emasligini tasdiqlash uchun ma'lumot konsolga chiqariladi.
Bu kod, deduktiv tekshirishning asosiy qismlarini ko'rsatadi, shu jumladan, funktsiyalar yaratish, amallar chaqirish va yordamchi o'zgaruvchilardan foydalanish.