NuSMV - NuSMV

NuSMV
Tuzuvchi (lar)FBK-irst (Trento, Italiya), CMU (Pitsburg, Pensilvaniya), The Jenova universiteti (Italiya), The Trento universiteti (Italiya)
Barqaror chiqish
2.6.0 / 2015 yil 14 oktyabr; 5 yil oldin (2015-10-14)
YozilganANSI C
Operatsion tizimLinux, Mac OS X, Microsoft Windows
TuriModelni tekshirish
LitsenziyaLGPL v2.1
Veb-saytnusmv.fbk.eu

NuSMV SMV-ning ramziy ma'nosini qayta tiklash va kengaytirishdir model tekshiruvchisi, asoslangan birinchi modelni tekshirish vositasi Ikkilik qarorlar diagrammasi (BDD).[1]Asbob an sifatida ishlab chiqilgan ochiq me'morchilik modelni tekshirish uchun. Bu sanoatdagi o'lchamlarni ishonchli tekshirishga, boshqa tekshirish vositalari uchun va tadqiqot vositasi sifatida foydalanish uchun mo'ljallangan. rasmiy tekshirish texnikalar.

NuSMV ITC-IRST (qo'shma loyiha) sifatida ishlab chiqilgan (Istituto Trentino di Cultura yilda Trento, Italiya ), Karnegi Mellon universiteti, Genuya universiteti va Trento universiteti.

NuSMV 2, NuSMV-ning 2-versiyasi, NuSMV-ning barcha funktsiyalarini meros qilib oladi. Bundan tashqari, u birlashadi BDD - asoslangan modelni tekshirish SAT - modelni tekshirish asosida.[2] Bu tomonidan saqlanadi Fondazione Bruno Kessler, ITC-IRST voris tashkiloti.

Funktsiyalar

NuSMV ko'rsatilgan xususiyatlarni tahlil qilishni qo'llab-quvvatlaydi CTL va LTL. Foydalanuvchilarning o'zaro ta'siri matnli interfeys bilan, shuningdek ommaviy rejim.

NuSMV-ni interaktiv ravishda ishga tushirish

NuSMV ning o'zaro ta'sir qobig'i tizim so'rovidan quyidagicha faollashtiriladi:

[system_prompt] $ NuSMV - kirishNuSMV> boringNuSMV>

NuSMV birinchi navbatda ishga tushirish faylidan buyruqlarni o'qishga va bajarishga harakat qiladi, agar bunday fayl mavjud bo'lsa va o'qisa -s buyruq satrida uzatiladi.File master.nusmvrc atrof-muhit o'zgaruvchisi NUSMV _LIBRARY_PATH-da belgilangan katalogdan yoki agar bunday o'zgaruvchi aniqlanmasa, standart kutubxona yo'lidan qidiriladi. Agar bunday fayl mavjud bo'lmasa, foydalanuvchining uy katalogi va joriy katalog ham tekshiriladi. Initsializatsiya faylidagi buyruqlar ketma-ket bajariladi. Ishga tushirish bosqichi tugagandan so'ng NuSMV qobig'i ko'rsatiladi va tizim foydalanuvchi buyruqlarini bajarishga tayyor.

NuSMV buyrug'i odatda buyruq nomi va chaqirilgan buyruqning argumentlaridan iborat. Buyruqlar satri opsiyasi orqali NuSMV-ni fayldan buyruqlar ketma-ketligini o'qish va bajarishni amalga oshirish mumkin -manba:

[system_prompt] $ NuSMV -sozlik cmd_file

NuSMV partiyasini ishga tushirish

-Int opsiyasi ko'rsatilmagan bo'lsa, NuSMV ommaviy dastur sifatida ishlaydi, u quyidagi shaklda:

[system_prompt] $ NuSMV [buyruq chiziq variantlari] kirish_fayli

LTL spetsifikatsiyasi yoki CTL spetsifikatsiyasini tekshirish

NuSMV oldindan belgilab qo'yilganligini tekshirish uchun ishlatilishi mumkin LTL yoki CTL Masalan, biz tekshirmoqchi bo'lgan CTL spetsifikatsiyasiga egamiz:

CTLSPECEF(pro5.davlat=tanqidiy);

Ushbu spetsifikatsiya, biron bir vaqtda 5-jarayonning holati juda muhim bo'lishi uchun ijro etish yo'lining mavjudligini tekshiradi va foydalanuvchi quyidagi buyruqlar yordamida ularning ushbu spetsifikatsiyaga mos kelishini tekshirishi mumkin.

[system_prompt] $ NuSMV [buyruq chiziq variantlari] kirish_fayliNuSMV> boringNuSMV> check_ctlspec

Agar spetsifikatsiya to'g'ri bo'lsa, NuSMV sizga xabar beradi

- spetsifikatsiyasi EF proc5.state = muhim to'g'ri>NuSMV

Ammo, agar spetsifikatsiya biron bir holatda ishlamay qolsa, NuSMV qanday bajarilmasligini ko'rsatib, to'liq bajarilishini izini qaytaradi.

Shuningdek qarang

  • Spin Model Checker asenkron dasturiy ta'minot tizimlari uchun umumiy model tekshirgich
  • SAPR (Taqsimlangan jarayonlarni qurish va tahlil qilish), asenkron bir vaqtda tizimlarning rasmiy dizayni uchun asboblar qutisi

Adabiyotlar

  1. ^ K.L. McMillan. Simvolli modelni tekshirish. Kluwer Academic Publ., 1993 y.
  2. ^ A. Bere, A. Cimatti, E. Klark va Y. Chju. BDD-larsiz ramziy modelni tekshirish. Tizimlarni qurish va tahlil qilish vositalari va algoritmlarida, TACAS’99 da, 1999 yil mart.

Tashqi havolalar