Abstraktsiya modelini tekshirish - Abstraction model checking

Bu maqola mavzu bilan tanish bo'lmaganlar uchun etarli bo'lmagan kontekstni taqdim etadi. Iltimos yordam bering maqolani takomillashtirish tomonidan o'quvchi uchun ko'proq kontekstni taqdim etish. (2009 yil oktyabr) (Ushbu shablon xabarini qanday va qachon olib tashlashni bilib oling)

Abstraktsiya modelini tekshirish faqat modelni ishlab chiqishda haqiqiy vakili juda murakkab bo'lgan tizimlar uchun. Shunday qilib, dizayn "abstrakt" versiyani kichraytirish uchun o'ziga xos tarjimani amalga oshiradi.

To'plami o'zgaruvchilar qiymatlarining o'zgarishiga qarab ko'rinadigan va ko'rinmaydigan qismlarga bo'linadi. Haqiqiy davlat maydoni ko'rinadiganlarning kichikroq to'plamiga qisqartiriladi.

Galois ulandi

Haqiqiy va mavhum holat bo'shliqlari Galois ulandi. Demak, agar biz elementni olsak mavhum bo'shliq, uni konkretlashtiring va konkretlashtirilgan versiyani mavhumlashtiring, natijada asl nusxaga teng bo'ladi. Boshqa tomondan, agar siz haqiqiy makondan element tanlasangiz, uni mavhumlashtirsangiz va mavhum versiyasini konkretlashtirsangiz, yakuniy natija asl nusxaning super to'plami bo'ladi.

Anavi,

${displaystyle eta}$(${displaystyle heta}$(mavhum)) = mavhum
${displaystyle heta}$(${displaystyle eta}$(haqiqiy)) ${displaystyle supseteq}$ haqiqiy

Abstraktsiyani takomillashtirish tsikli

Abstraktatsiya bilan bog'liq muammo modelni tekshirish shundan iboratki, abstrakt realni simulyatsiya qilsa-da, abstrakt xususiyatni qondirmasa, demak, bu xususiyat haqiqiy modelda haqiqatan ham ishlamay qolishini anglatmaydi. Qarama-qarshi misollar haqiqiy holat maydoniga qarab tekshiriladi, chunki biz "soxta" hisoblagich misollarni olamiz. Shunday qilib, abstraktsiyani takomillashtirish tsiklining bir qismi:

1. Mavhum modelni oling
2. Modelni tekshiring va hamma narsa yaxshi yoki yo'qligini tekshiring.
3. Agar qarama-qarshi misol mavjud bo'lsa, haqiqiy holat maydoniga qayting va aslida hisoblagich modeli ekanligini bilib oling.
4. Agar yo'q bo'lsa, qaytib keling va modelni tekshirishni davom eting.

Soxta misollar asosan o'lik holatlar va yomon holatlar bir xil mavhum bo'lganligi sababli hosil bo'ladi. Buni hal qilish uchun biz ikkita tur o'rtasida ajratish yaratishimiz kerak. Keyingi qadam, aslida o'lik va yomon holatlar o'rtasida farq qiladigan ko'rinmas o'zgaruvchilarning pastki qismini topish va ushbu qismni ko'rinadigan yoki kuzatiladigan o'zgaruvchilar to'plamiga qo'shishdir. Agar ajratish qimmatga tushsa, aniqlik namunalardan o'rganishga asoslangan bo'lishi mumkin.

Adabiyotlar

• Edmund M. Klark va Orna Grumberg va Devid E. Long (1994). "Modelni tekshirish va abstraktsiya". Dasturlash tillari va tizimlari bo'yicha ACM operatsiyalari. 16 (5): 1512–1542. CiteSeerX  10.1.1.79.3022. doi:10.1145/186025.186051.