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

Download 15.82 Kb.
bet	1/2
Sana	17.04.2024
Hajmi	15.82 Kb.
	#199017

Bog'liq
Rasmiy (ekvivalentlikni tekshirish, modelni tekshirish, deduktiv-fayllar.org
Taqdimoti mavzu umumiy tipdagi davlat va nodavlat maktabgacha t-fayllar.org, Essey, U1910127, HospitaLogix, 3-mavzuTBamaliy, ELEKTRON TIJORATNING HUQUQIY ASOSLARI kurs (5), Kurs ishi, namuna amaliyot dars reja, dars reja namuna(nazariy), аммамнинг таквими арм заоч, Кутубхонашунослик, Презентация1, ЎРҚ-410 22.09.2016, 8-lectures Presentation tech (1)

Bu sahifa navigatsiya:

• UNIVERSITETI SAMARQAND FILIALI

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. Download 15.82 Kb.

Download 15.82 Kb.