Bog'liq Dasturiy injiniringga kirish Ma\'ruza 2022-03-11
Formal usullar va ishnchlilik Dasturiy ta'minotni ishlab chiqishda matematik rasmiy yondashuvdan foydalanish informatika rivojlanishining dastlabki bosqichida taklif qilingan. Rasmiy spetsifikatsiya va dastur mustaqil ravishda ishlab chiqilishi mumkin edi. Keyin dastur va uning spetsifikatsiyasi izchil ekanligini ko'rsatish uchun matematik dalil ishlab chiqilishi mumkin. Dastlab, dalillar qo'lda ishlab chiqilgan, ammo bu uzoq va qimmat jarayon edi. Qo'lda dalillarni faqat juda kichik tizimlar uchun ishlab chiqish mumkinligi tezda ma'lum bo'ldi. Dasturni isbotlash endi keng ko'lamli avtomatlashtirilgan teoremani isbotlovchi dasturiy ta'minot bilan qo'llab-quvvatlanadi, bu esa kattaroq tizim ildizlarini isbotlash imkonini beradi. Biroq, teorema isbotlovchilari uchun isbot majburiyatlarini ishlab chiqish qiyin va maxsus vazifadir, shuning uchun rasmiy tekshirish keng qo'llanilmaydi.
Dasturiy ta'minot injiniringining rasmiy usullari dasturiy ta'minot ko'rinishidagi xatolarning ikki sinfini aniqlash yoki oldini olish uchun samarali bo'ladi:
Spetsifikatsiya va dizayndagi xatolar va kamchiliklar. Dasturiy ta'minotning rasmiy modelini ishlab chiqish va tahlil qilish jarayoni dasturiy ta'minot talablarida xato va kamchiliklarni aniqlashi mumkin. Agar model avtomatik yoki tizimli ravishda manba kodidan yaratilgan bo'lsa, modelni tekshirish yordamida tahlil ro'y berishi mumkin bo'lgan istalmagan holatlarni aniqlashi mumkin, masalan, bir vaqtning o'zida tizimdagi boshi berk ko'cha.
Spetsifikatsiya va dastur o'rtasidagi nomuvofiqliklar. Agar takomillashtirish usuli qo'llanilsa, dasturiy ta'minotni spetsifikatsiyaga mos kelmaydigan ishlab chiquvchilar tomonidan qilingan xatolar oldini oladi. Dasturni isbotlash dastur va uning spetsifikatsiyasi o'rtasidagi nomuvofiqlikni aniqlaydi.
Barcha rasmiy usullarning boshlang'ich nuqtasi tizim spetsifikatsiyasi vazifasini bajaradigan matematik tizim modelidir. Ushbu modelni yaratish uchun siz tizimning tabiiy tilda, diagramma va jadvallarda ifodalangan foydalanuvchi talablarini rasmiy ravishda aniqlangan semantikaga ega matematik tilga tarjima qilasiz. Rasmiy spetsifikatsiya tizim nima qilishi kerakligining aniq tavsifidir.
Rasmiy spetsifikatsiyani ishlab chiqish va uni rasmiy ishlab chiqish jarayonida qo'llashning afzalliklari quyidagilardan iborat:
Rasmiy spetsifikatsiyani batafsil ishlab chiqishda siz tizim talablarini chuqur va batafsil tushunishni rivojlantirasiz. Erta ko'rib chiqilgan talablar bilan bog'liq muammolar, odatda, rivojlanish jarayonining keyingi bosqichlarida topilganidan ko'ra, ularni tuzatish ancha arzon .
Spetsifikatsiya rasmiy ravishda belgilangan semantikaga ega tilda ifodalanganligi sababli, nomuvofiqliklar va to'liqsizliklarni aniqlash uchun uni avtomatik ravishda tahlil qilishingiz mumkin.
Agar siz B usuli kabi usuldan foydalansangiz, to'g'rilikni saqlaydigan transformatsiyalar ketma-ketligi orqali rasmiy spetsifikatsiyani dasturga aylantirishingiz mumkin . Shunday qilib, natijada olingan dastur uning spetsifikatsiyasiga javob berishi kafolatlanadi.
Dasturni sinovdan o'tkazish xarajatlari kamayishi mumkin, chunki siz dasturni uning spetsifikatsiyasiga muvofiq tekshirgansiz. Misol uchun, Parij metro tizimlari uchun dasturiy ta'minotni ishlab chiqishda, takomillashtirishdan foydalanish dasturiy ta'minot komponentlarini sinovdan o'tkazishning hojati yo'qligini va faqat tizim testini o'tkazish kerakligini anglatardi.
Ushbu afzalliklarga qaramay, rasmiy usullar hatto muhim tizimlar uchun ham amaliy dasturiy ta'minotni ishlab chiqishga cheklangan ta'sir ko'rsatdi. Vudkok 25 yil davomida rasmiy usullardan foydalangan 62 loyiha haqida hisobot beradi. Agar biz ushbu usullardan foydalangan, lekin ulardan foydalanish haqida xabar bermagan loyihalarga ruxsat bergan bo'lsak ham, bu o'sha paytda ishlab chiqilgan muhim tizimlar umumiy sonining kichik bir qismidir. Sanoat bir qator sabablarga ko'ra rasmiy usullarni qo'llashni istamaydi:
Muammo egalari va domen mutaxassislari rasmiy spetsifikatsiyani tushuna olmaydilar, shuning uchun ular uning talablarini to'g'ri ko'rsatishini tekshira olmaydilar. Rasmiy spetsifikatsiyani tushunadigan dasturiy ta'minot muhandislari dastur domenini tushunmasligi mumkin, shuning uchun ular ham rasmiy spetsifikatsiya tizim talablarining to'g'ri aks etishiga ishonch hosil qila olmaydi.
Rasmiy spetsifikatsiyani yaratish xarajatlarini hisoblash juda oson, lekin undan foydalanish natijasida yuzaga kelishi mumkin bo'lgan xarajatlarni tejashni hisoblash qiyinroq. Natijada, menejerlar rasmiy usullarni qo'llash xavfini o'z zimmalariga olishni xohlamaydilar. Muvaffaqiyat to'g'risidagi hisobotlar ularni ishontirmaydi, chunki ular asosan ishlab chiquvchilar rasmiy yondashuv tarafdori bo'lgan atipik loyihalardan kelib chiqqan.
Ko'pgina dasturiy ta'minot muhandislari rasmiy spetsifikatsiya tillaridan foydalanishga o'rgatilmagan . Shuning uchun ular rivojlanish jarayonlarida ulardan foydalanishni taklif qilishni istamaydilar.
Hozirgi rasmiy usullarni juda katta tizimlargacha kengaytirish qiyin. Rasmiy usullardan foydalanilganda, u asosan to'liq tizimlarni emas, balki muhim yadro dasturlarini belgilash uchun ishlatiladi.
Rasmiy usullar uchun asboblarni qo'llab-quvvatlash cheklangan va mavjud vositalar ko'pincha ochiq manba va ulardan foydalanish qiyin. Bozor tijorat vositalarini etkazib beruvchilar uchun juda kichik.
Rasmiy usullar, dasturlar bosqichma-bosqich ishlab chiqiladigan tezkor rivojlanish bilan mos kelmaydi. Biroq, bu muhim muammo emas, chunki aksariyat muhim tizimlar hali ham rejaga asoslangan yondashuv yordamida ishlab chiqilgan.
Rasmiy rivojlanishning dastlabki tarafdori Parnas hozirgi rasmiy usullarni tanqid qildi va ular tubdan noto'g'ri asosdan boshlangan deb da'vo qildi (Parnas 2010). Uning fikricha, bu usullar tubdan soddalashtirilmaguncha qabul qilinmaydi, buning uchun matematikaning boshqa turi asos sifatida talab qilinadi. Mening fikrimcha, bu hatto boshqa dasturiy injiniring usullari bilan solishtirganda ularni qabul qilish va ulardan foydalanish iqtisodiy jihatdan samarali ekanligini aniq ko'rsatmasa, muhim tizim muhandisligi uchun rasmiy usullar muntazam ravishda qabul qilinadi degani emas.
