Seznam nástrojů pro kontrolu modelů - List of model checking tools

Tento článek uvádí kontrola modelu nástroje a dává syntetický přehled o jejich funkcích.

Přehled některých nástrojů pro kontrolu modelu

Následující tabulka obsahuje modeláře, kteří mají

(1) webovou stránku, ze které lze stáhnout,

(2) deklarovanou licenci,

(3) popis zveřejněný v archivované literatuře a

(4) článek z Wikipedie, který to popisuje.

V následující tabulce jsou použity následující zkratky:

• Ekvivalence:
  • SB: Silná bisimulace
  • WB: Slabá bisimulace
  • BB: Větvení bisimulace
  • STE: Silná stopová ekvivalence
  • WTE: Slabá stopová ekvivalence
  • já: May Equivalence
  • ME: Must Equivalence
  • OE: Pozorovací ekvivalence
  • SE: Rovnocennost bezpečnosti
  • t * E: tau * .a Rovnocennost
• Softwarová licence:
  • FUSC: Zdarma za určitých podmínek (např. Zdarma pro akademické pracovníky)

Modelovací jazyky

• CCSP: Procesní kalkul získaný z CCS začleněním některých provozovatelů CSP. Definuje to Olderog^[1] a van Glabbeek / Vaandrager.^[2]
• CSP: Komunikace sekvenčních procesů; formální jazyk pro popis vzorů interakce v souběžných systémech. FDR2 je nástroj pro zdokonalení kontroly pro CSP, který porovnává dva modely z hlediska kompatibility.
• Vstupní jazyk DVE: systém je popsán jako síť rozšířených strojů konečného stavu komunikujících prostřednictvím sdílených proměnných a kanálů bez vyrovnávací paměti. Neobsahuje podporu pro kanály v mezipaměti a pro kontrolu typu zprávy, která má být přijata, aniž by provedla správné přijetí.
• FC2: (Common Format V2) Reprezentace ASCII na úrovni stroje pro synchronizované (hierarchické) sítě automatů. Definováno akcí Esprit Basic Research Action CONCUR, 1992. Používá se jako vstupní a výměnný formát řadou ověřovacích nástrojů, zejména v oblasti procesních algeber.
• FSP: Finite State Processes language definovaný na Imperial College.
• Jáva: Objektově orientovaný programovací jazyk.
• LNT: LOTOS nová technologie; specifikační jazyk inspirovaný procesními kalkulemi, funkčními programovacími jazyky a imperativním programovacím jazykem; LNT byl navržen jako moderní náhrada za LOTOS a E-LOTOS.
• LOTOS: Specifikace jazyka dočasného objednání (norma ISO 8807); jazyk formální specifikace založený na časovém uspořádání použitý pro specifikaci protokolu v normách ISO OSI.
• PEPA: Algebra procesu hodnocení výkonu; je to stochastická procesní algebra určená pro modelování počítačových a komunikačních systémů.
• Plain MC: jednoduché formáty textových souborů používané v MRMC a PRISM.
• Promela: Meta jazyk procesu nebo protokolu; je to ověřovací modelovací jazyk. Jazyk umožňuje dynamické vytváření souběžných procesů k modelování například distribuovaných systémů.
• TLA +: Univerzální specifikační jazyk založený na časové logice akcí, původně používaný pro distribuované a souběžné systémy. Jazyk specifikací a jejich vlastností je stejný.

Vlastnosti

• AFMC: Bez střídání modální μ-kalkul.
• Tvrzení: Prohlášení imperativního tvrzení.
• CSL: Continuous Stochastic Logic, charakterizuje bisimulaci kontinuálních Markovových procesů.
• CSRL: Continuous Stochastic Reward Logic; logika specifikující míry nad CTMC rozšířená o strukturu odměn (tzv. Markovovy modely odměn).
• CTL: Logika výpočetního stromu; logika větvícího času, což znamená, že jeho model času je stromová struktura, ve které není určena budoucnost; v budoucnu existují různé cesty, z nichž každá může být skutečnou cestou, která je realizována.
• LTL: Lineární temporální logika; modální časová logika s modalitami odkazujícími na čas.
• MCL: Model Checking Language; Bez střídání Modální μ-kalkul rozšířeno o uživatelsky přívětivé regulární výrazy a konstrukty předávající hodnotu; subsumy CTL a LTL.
• mCRL2 mu-počet: Kozenův výrok modální μ-kalkul (kromě atomových propozic), rozšířeno o: procesy závislé na datech, kvantifikace přes datové typy, multi-akce, čas a pravidelné vzorce.
• PCTL: Pravděpodobnostní CTL; rozšíření CTL, které umožňuje pravděpodobnostní kvantifikaci popsaných vlastností.
• PLTL: Pravděpodobnostní lineární časová logika.
• PRCTL: Pravděpodobnostní logika stromu výpočtu odměn; rozšiřuje se PCTL s vlastnostmi ohraničenými odměnou.
• PSL: Jazyk specifikace vlastnosti
• SVA: SystemVerilog podmnožina jazyka pro uplatnění norem, standardizovaná jako IEEE 1800
• XTL: eXtended Temporal Language; jazyk specifický pro doménu pro rychlou implementaci kontrolních modelů založených na akcích, explicitním stavu a předávání hodnot.

Porovnání nástrojů pro kontrolu modelu

Vědecké publikace

Existuje několik článků, které systematicky porovnávají různé modely kontroly na společné případové studii. Srovnání obvykle pojednává o kompromisech modelování, kterým čelí při použití vstupních jazyků každého modelu kontroly, a také o srovnání výkonů nástrojů při ověřování vlastností správnosti. Lze zmínit:

• V roce 1999 Judi Romijn porovnala dva modely dámy (CADP a ROZTOČIT ) o interoperabilitě audio-video protokolu HAVi pro spotřební elektroniku.^[3]

• V roce 2003 Yifei Dong, Xiaoqun Du, Gerard J. Holzmann a Scott A. Smolka zveřejnili srovnání čtyř modelových dám (jmenovitě: Cospan, Murphi, ROZTOČIT a XMC) na komunikačním protokolu, GNU i-protokolu.^[4]

• V roce 2005 publikovali Elena M. Bortnik, Nikola Trcka, Anton Wijs, Bas Luttik, J. M. van de Mortel-Fronczak, Jos C. M. Baeten, Wan Fokkink a J. E. Rooda srovnání čtyř modelových dám (jmenovitě: CADP, muCRL, ROZTOČIT, a UPPAAL ) na systému průmyslové výroby, rotační vrtačku.^[5]

• V roce 2018 publikovali F. Mazzanti a A. Ferrari srovnání deseti modelových dám (jmenovitě: CADP Nástroje CPN, FDR4, NuSMV / nuXmv, mCRL2, ProB, ROZTOČIT, TLA +, UMC a UPPAAL ) o problému dohledu nad vlakem, s přihlédnutím jak k uživatelské přívětivosti jazyků, tak k výkonu nástrojů.^[6]

Mezinárodní softwarové soutěže

• Od roku 2007 Soutěž o kontrolu hardwarového modelu (HWMCC) porovnává výkonnost nástrojů pro kontrolu modelů orientovaných na návrh hardwaru.
• Od roku 2011 Soutěž o kontrolu modelu (MCC) porovnávají výkon nástrojů pro kontrolu modelů určených k analýze vysoce souběžných systémů.

Společné referenční hodnoty

• MCC (modely soutěže Model Checking Contest): sbírka stovek Petriho sítí pocházející z mnoha akademických a průmyslových případových studií.
• VLTS (Very Large Transition Systems): sbírka označených přechodových systémů rostoucí velikosti, používaných v mnoha vědeckých publikacích.

Reference

externí odkazy

• Nástroje: databáze nástrojů pro ověřování
• Seznam nástrojů pro ověření a syntézu (public domain repository on GitHub)
• Seznam ověřovacích nástrojů pro pravděpodobnostní, stochastické, hybridní a časované systémy

Ostatní modeláři, kteří ještě nemají stránku Wikipedie:

• AcPeg,
• AlPiNA,
• Kontrola AltaRica (ARC),
• APMC,
• BANDERA,
• BOGOR,
• CADENCE SMV,
• CMurphi,
• CBMC,
• CWB-NC,
• BOŽSKÝ,
• DSVerifier,
• EBMC,
• Edinburgh CWB,
• EmbeddedValidator,
• ESBMC,
• Expander2,
• Fc2Tools,
• OZUBENÉ KOLO,
• Kronos,
• Zlepšit,
• Intrepyd,
• JasperGold,
• LLBMC,
• LTSA,
• μCRL,
• Marcie,
• McErlang,
• MCMAS,
• Náměsíčný,
• nuXmv,
• ompca,
• ProB,
• PMC,
• PSCV,
• Kontrola vlastnosti Questa (PropCheck),
• Reactis Tester,
• ČERVENÉ,
• SAL,
• SATABS,
• SATMC,
• SLMC,
• CHYTRÝ,
• Bod,
• SSG,
• SyncStitch,

a

• Tina.