"Kompyuter injiniring" fakulteti "Kampyuter tizimlar" kafedrasi "Dastur tekshirish farmal usullari ” fanidan 1-labaratoriya Mavzu: Ketma-ket dasturlarni deduktiv tekshirish

---

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-labaratoriya 
Mavzu: Ketma-ket dasturlarni deduktiv tekshirish 
 
 
 
 
 
 
Bajardi :Ramatov M 
 
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.