|
1-Amaliy Ish Bajardi: Boboraximov N
|
| bet | 1/2 | | Sana | 17.04.2024 | | Hajmi | 1.03 Mb. | | #198697 |
Bog'liq formal 1-lab.ish KM 3032101310, Sanoat ekоlоgiyasi va hayot faoliyati xavfsizligi amaliy mashg\'uloti, AXBOROT XATI-2024-1-scholar, 3-mavzu. Chiziqli tenglamalar sistemasi, usanov-mamadali-1-m
MUHAMMAD AL-XORAZMIY NOMIDAGI TOSHKENT AXBOROT TEXNOLOGIYALARI UNIVERSITETI SAMARQAND FILIALI
“KOMPYUTER INJINIRINGI” FAKULTETI
”Dasturni tekshirishning formal usullari”
Fanidan
1-Amaliy Ish
Bajardi: Boboraximov N.
Fan o‘qituvchisi: SAYDULLAYEV E.
SAMARQAND _ 2024
MAVZU: Dasturni tekshirishning rasmiy usullari. Dasturlash tillari semantikasini rasmiylashtirish. Ketma-ket dasturlarni deduktiv tekshirish.
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. 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.
|
| |
