Formal verification — dastur, protokol yoki apparat modelining belgilangan xususiyatlarga mosligini matematik mantiq va avtomatlashtirilgan isbot vositalari yordamida tekshirish jarayonidir. U test kabi ayrim input namunalarini emas, model doirasidagi barcha holat yoki executionlarni qamrab olishga intiladi. Natija spetsifikatsiya va taxminlar to‘g‘ri bo‘lgandagina mazmunli.
Spetsifikatsiya
Avval tizimdan kutilgan property formal yoziladi. Safety “yomon holat hech qachon bo‘lmaydi”, liveness esa “kerakli holat oxir-oqibat yuz beradi” degan xususiyatdir. Masalan, ikki node bir vaqtda leader bo‘lmasligi safety, so‘rovning bir kun kelib javob olishi liveness bo‘lishi mumkin.
Noto‘g‘ri yoki yetarli bo‘lmagan specification uchun mukammal proof ham noto‘g‘ri maqsadni isbotlaydi. Requirement review va domain ekspert ishtiroki formal ishning qismidir.
Model checking
Model checker finite state modelning barcha reachable holatlarini ko‘rib property buzilishini qidiradi. Buzilish topilsa counterexample execution trace beradi. Bu distributed protocol, state machine va concurrency interleavinglarini tahlil qilishda foydali.
State explosion node, message va variable soni oshganda holatlar keskin ko‘payishini anglatadi. Abstraction, symmetry reduction va bounded model checking qidiruvni boshqaradi. Cheklangan modeldagi isbot real cheksiz tizimga avtomatik ko‘chmaydi.
Theorem proving
Interactive theorem prover dastur va property haqida lemma hamda proof qurishga imkon beradi. Induction cheksiz struktura yoki executionni qamrashi mumkin. Proof assistant kichik trusted kernel orqali isbot termlarini tekshiradi.
SMT solver logical formula va constraintni avtomatik hal qilib, symbolic execution va verification conditionlarni tekshiradi. Solver unknown qaytarishi yoki timeout bo‘lishi mumkin; bu property false degani emas. Solver version va axiomlar proof artefaktiga kiradi.
Program verification
Precondition funksiya chaqirilishidan oldingi, postcondition keyingi talabni bildiradi. Loop invariant har iteratsiyada saqlanadigan property bo‘lib, correctness isbotining asosidir. Frame condition qaysi state o‘zgarishi mumkinligini cheklaydi.
Memory safety, absence of overflow yoki access-control invariant formal tekshirilishi mumkin. External library, compiler va hardware trusted computing base bo‘lib qolishi mumkin. Verified source’dan unverified build natijasi o‘rtasidagi bo‘shliqni verified compiler yoki translation validation kamaytiradi.
Amaliy qo‘llash
Formal verification eng kritik, kichik yadroga yo‘naltirilishi mumkin: consensus protocol, cryptographic primitive yoki authorization policy. Qolgan tizim test, static analysis va runtime monitoring bilan himoyalanadi. Bu xarajat va xavfga mutanosib yondashuvdir.
Model va implementation drift qilmasligi uchun specification repositoryda versionlanadi, CI propertyni tekshiradi va code mapping hujjatlanadi. Proof “bir marta tugagan hujjat” emas; requirement o‘zgarsa u ham yangilanadi.
Proof chegarasi
Verification hisobotida aynan qaysi property, model va trusted assumption qamralgani yoziladi. “Formal verified” umumiy marketing iborasi barcha xavfsizlik xususiyati isbotlanganini anglatmaydi. Timing side channel, hardware fault yoki operator configuration modeldan tashqarida qolishi mumkin.
Proof review source code reviewdan farqli bilim talab qiladi. Machine-checked artefakt human specification xatosini topmaydi, shu sabab property independent review va adversarial misollar bilan sinovdan o‘tadi. Counterexample real bugga aylantirilganda regression test ham qo‘shiladi. Formal va dynamic test bir-birini almashtirmay, turli xato sinfini qamrab oladi.
Reproducibility uchun prover versiyasi, dependencylar, solver parametrlari va proof script saqlanadi. Build muhitini qayta tiklash imkoni bo‘lmasa machine-checked natijani keyinchalik mustaqil tasdiqlash qiyinlashadi.
Bog‘liq tushunchalar
Model checking, Theorem proving, Formal specification, Invariant, SMT solver, Hoare logic, Program correctness