NuSMV - NuSMV

NuSMV
Geliştirici (ler)FBK-ilk (Trento, İtalya), CMU (Pittsburgh, PA), The Genova Üniversitesi (İtalya), The Trento Üniversitesi (İtalya)
Kararlı sürüm
2.6.0 / 14 Ekim 2015; 5 yıl önce (2015-10-14)
YazılmışANSI C
İşletim sistemiLinux, Mac OS X, Microsoft Windows
TürModel Kontrolü
LisansLGPL v2.1
İnternet sitesinusmv.fbk.eu

NuSMV yeniden uygulama ve SMV sembolik uzantısıdır model denetleyicisi ilk model kontrol aracıdır. İkili Karar Diyagramları (BDD'ler).[1]Araç, bir açık mimari model kontrolü için. Diğer doğrulama araçları için bir arka uç olarak ve diğer doğrulama araçları için bir araştırma aracı olarak kullanılmak üzere endüstriyel olarak boyutlandırılmış tasarımların güvenilir şekilde doğrulanması amaçlanmıştır. resmi doğrulama teknikleri.

NuSMV, ITC-IRST arasında ortak bir proje olarak geliştirilmiştir (Istituto Trentino di Cultura içinde Trento, İtalya ), Carnegie Mellon Üniversitesi, Cenova Üniversitesi ve Trento Üniversitesi.

NuSMV 2NuSMV sürüm 2, NuSMV'nin tüm işlevlerini devralır. Dahası, birleştirir BDD tabanlı model kontrolü OTURDU tabanlı model kontrolü.[2] Tarafından korunur Fondazione Bruno Kessler, ITC-IRST'nin halef organizasyonu.

İşlevsellikler

NuSMV, aşağıda belirtilen özelliklerin analizini destekler CTL ve LTL. Kullanıcı etkileşimi, metinsel bir arayüzle ve ayrıca toplu modu.

NuSMV'yi Etkileşimli Olarak Çalıştırma

NuSMV'nin etkileşim kabuğu, sistem komut isteminden aşağıdaki şekilde etkinleştirilir:

[system_prompt] $ NuSMV -intNuSMV> gitNuSMV>

NuSMV, eğer böyle bir dosya mevcutsa ve bu tür bir dosya mevcutsa ve bu tür bir dosya yoksa -s komut satırına aktarılır. master.nusmvrc dosyası, NUSMV _LIBRARY_PATH ortam değişkeninde tanımlanan dizinde veya böyle bir değişken tanımlanmamışsa varsayılan kitaplık yolunda aranır. Böyle bir dosya yoksa, kullanıcının ev dizini ve mevcut dizini de kontrol edilecektir. Başlatma dosyasındaki komutlar ardışık olarak yürütülür. Başlatma aşaması tamamlandığında NuSMV kabuğu görüntülenir ve sistem artık kullanıcı komutlarını yürütmeye hazırdır.

Bir NuSMV komutu genellikle bir komut adı ve çağrılan komutun argümanlarından oluşur. Komut satırı seçeneği aracılığıyla NuSMV'nin bir dosyadan bir dizi komut okumasını ve yürütmesini sağlamak mümkündür. -kaynak:

[system_prompt] $ NuSMV -kaynak cmd_file

NuSMV toplu işlemini çalıştırma

-İnt seçeneği belirtilmediğinde, NuSMV aşağıdaki formda bir toplu iş programı olarak çalışır:

[system_prompt] $ NuSMV [komut hat seçenekleri] giriş dosyası

LTL spesifikasyonunun veya CTL spesifikasyonunun kontrol edilmesi

NuSMV, önceden tanımlanmış olup olmadığını kontrol etmek için kullanılabilir. LTL veya CTL kısıtlamalar tanımlanan model için geçerlidir.Örneğin, kontrol etmek istediğimiz bir CTL spesifikasyonumuz var:

CTLSPECEF(proc5.durum=kritik);

Bu belirtim, işlem 5'in durumu bir noktada kritik olacak şekilde bir yürütme yolu olup olmadığını kontrol eder. Kullanıcı, aşağıdaki komutları kullanarak modelinin bu belirtim için geçerli olup olmadığını kontrol edebilir.

[system_prompt] $ NuSMV [komut hat seçenekleri] giriş dosyasıNuSMV> gitNuSMV> check_ctlspec

Spesifikasyon doğruysa, NuSMV sizi bilgilendirecektir

- belirtim EF proc5.state = kritik doğru>NuSMV

Ancak, belirtim bazı durumlarda başarısız olursa, NuSMV nasıl başarısız olduğunu gösteren tam bir yürütme izi döndürür.

Ayrıca bakınız

  • Döndürme Modeli Denetleyicisi asenkron yazılım sistemleri için genel bir model denetleyicisi
  • CADP (Dağıtık Süreçlerin Oluşturulması ve Analizi), eşzamansız eşzamanlı sistemlerin resmi tasarımı için bir araç kutusu

Referanslar

  1. ^ K.L. McMillan. Sembolik model kontrolü. Kluwer Academic Publ., 1993.
  2. ^ A. Biere, A. Cimatti, E. Clarke ve Y. Zhu. BDD'ler olmadan sembolik model kontrolü. Sistemlerin İnşası ve Analizi için Araçlar ve Algoritmalar içinde, TACAS’99'da, Mart 1999.

Dış bağlantılar