Konstrukce a analýza distribuovaných procesů - Construction and Analysis of Distributed Processes

Konstrukce a analýza distribuovaných procesů
Cadp logo.gif
VývojářiINRIA CONVECS tým (dříve VASY tým)
První vydání1989, před 30–31 lety
Stabilní uvolnění
2018 / 13. prosince 2018; Před 23 měsíci (2018-12-13)
Operační systémOkna, Operační Systém Mac, Linux, Solaris, a OpenIndiana
TypSada nástrojů pro návrh komunikačních protokolů a distribuovaných systémů
webová stránkacadp.inria.fr

CADP[1] (Konstrukce a analýza distribuovaných procesů) je sada nástrojů pro návrh komunikačních protokolů a distribuovaných systémů. CADP je vyvíjen týmem CONVECS (dříve týmem VASY) na adrese INRIA Rhone-Alpes a připojeno k různým doplňkovým nástrojům. CADP je udržován, pravidelně vylepšován a používán v mnoha průmyslových projektech.

Účelem sady nástrojů CADP je usnadnit návrh spolehlivých systémů pomocí technik formálního popisu spolu se softwarovými nástroji pro simulaci, rychlý vývoj aplikací, ověřování a generování testů.

CADP lze použít na jakýkoli systém, který obsahuje asynchronní souběžnost, tj. Na jakýkoli systém, jehož chování lze modelovat jako sadu paralelních procesů řízených sémantikou prokládání. Proto lze CADP použít k návrhu hardwarové architektury, distribuovaných algoritmů, telekomunikačních protokolů atd. Techniky enumerativního ověřování (známé také jako ověřování explicitního stavu) implementované v CADP, i když méně obecné než dokazování věty, umožňují automatickou a nákladově efektivní detekci konstrukčních chyb ve složitých systémech.

CADP obsahuje nástroje na podporu použití dvou přístupů ve formálních metodách, které jsou oba potřebné pro spolehlivý návrh systémů:

  • Modely poskytují matematická znázornění paralelních programů a souvisejících ověřovacích problémů. Příkladem modelů jsou automaty, sítě komunikujících automatů, Petriho sítě, binární rozhodovací diagramy, systémy booleovských rovnic atd. Z teoretického hlediska hledá výzkum modelů obecné výsledky, nezávislé na konkrétním popisném jazyce.
  • V praxi jsou modely často příliš elementární na to, aby přímo popisovaly složité systémy (bylo by to zdlouhavé a náchylné k chybám). Formalismus vyšší úrovně známý jako zpracovat algebru nebo procesní kalkul pro tento úkol, stejně jako kompilátory, které překládají popisy na vysoké úrovni do modelů vhodných pro ověřovací algoritmy.

Dějiny

Práce na CADP byly zahájeny v roce 1986, kdy byl zahájen vývoj prvních dvou nástrojů, CAESAR a ALDEBARAN. V roce 1989 byla vytvořena zkratka CADP, což znamenalo Distribuční balíček CAESAR / ALDEBARAN. Postupem času bylo přidáno několik nástrojů, včetně programovacích rozhraní umožňujících přispění nástrojů: zkratka CADP se poté stala Vývojový balíček CAESAR / ALDEBARAN. V současné době CADP obsahuje více než 50 nástrojů. Při zachování stejné zkratky byl název sady nástrojů změněn, aby lépe určoval jeho účel:Konstrukce a analýza distribuovaných procesů.

Hlavní zprávy

Úniky CADP byly postupně pojmenovány abecedními písmeny (od „A“ do „Z“), poté názvy měst, kde se nacházejí akademické výzkumné skupiny aktivně pracující na LOTOS jazyk a obecněji názvy měst, do kterých významně přispívají teorie souběžnosti byl vyroben.

Krycí jménodatum
„A“ ... „Z“Leden 1990 - prosinec 1996
TwenteČerven 1997
LiegeLeden 1999
OttawaČervenec 2001
EdinburghProsinec 2006
Curychprosinec 2013
AmsterdamProsince 2014
Stony BrookProsinec 2015
OxfordProsinec 2016
Sophia AntipolisProsince 2017
UppsalaProsince 2018
PisaProsince 2019

Mezi hlavními verzemi jsou často k dispozici menší verze, které poskytují včasný přístup k novým funkcím a vylepšením. Další informace viz seznam změn stránka na webu CADP.

Funkce CADP

CADP nabízí širokou škálu funkcí, od postupné simulace po masivně paralelní kontrola modelu. To zahrnuje:

  • Překladače několika vstupních formalismů:
    • Popisy protokolů na vysoké úrovni psané v jazyce ISO LOTOS.[2] Sada nástrojů obsahuje dva kompilátory (CAESAR a CAESAR.ADT), které překládají popisy LOTOS do kódu C a používají se pro účely simulace, ověření a testování.
    • Popisy protokolu na nízké úrovni určené jako stroje s konečným stavem.
    • Sítě komunikačních automatů, tj. Stroje s konečným stavem běžící paralelně a synchronizované (buď pomocí operátorů algebry procesu nebo synchronizačních vektorů).
  • Několik kontrola rovnocennosti nástroje (minimalizace a srovnání modulo bisimulačních vztahů), jako BCG_MIN a BISIMULATOR.
  • Několik kontrolerů modelů pro různé časové logiky a mu-kalkulů, například EVALUATOR a XTL.
  • Kombinace několika ověřovacích algoritmů: enumerativní ověření, ověřování on-the-fly, symbolické ověřování pomocí binárních rozhodovacích diagramů, minimalizace kompozice, částečné objednávky, kontrola distribuovaného modelu atd.
  • Plus další nástroje s pokročilými funkcemi, jako je vizuální kontrola, hodnocení výkonu atd.

CADP je navržen modulárně a klade důraz na přechodné formáty a programovací rozhraní (například softwarové prostředí BCG a OPEN / CAESAR), které umožňují kombinovat nástroje CADP s jinými nástroji a přizpůsobovat je různým specifikačním jazykům.

Modely a techniky ověřování

Ověření je srovnání komplexního systému s množinou vlastností charakterizujících zamýšlené fungování systému (například svoboda uváznutí, vzájemné vyloučení, spravedlnost atd.).

Většina ověřovacích algoritmů v CADP je založena na modelu označených přechodových systémů (nebo jednoduše automatů nebo grafů), který se skládá ze sady stavů, počátečního stavu a přechodového vztahu mezi stavy. Tento model je často generován automaticky z popisů vysoké úrovně studovaného systému, poté je porovnáván s vlastnostmi systému pomocí různých rozhodovacích postupů. V závislosti na formalismu použitém k vyjádření vlastností jsou možné dva přístupy:

  • Vlastnosti chování vyjadřují zamýšlené fungování systému ve formě automatů (nebo popisů na vyšší úrovni, které jsou poté převedeny do automatů). V takovém případě je přirozený přístup k ověření kontrola rovnocennosti, který spočívá v porovnání modelu systému a jeho vlastností (oba reprezentovaných jako automaty) modulo nějakou ekvivalenci nebo předobjednávku vztahu. CADP obsahuje nástroje pro kontrolu ekvivalence, které porovnávají a minimalizují automaty modulo různé ekvivalence a předobjednávky; některé z těchto nástrojů platí také pro stochastické a pravděpodobnostní modely (například Markovovy řetězce). CADP také obsahuje vizuální kontrola nástroje, které lze použít k ověření grafického znázornění systému.
  • Logické vlastnosti vyjadřují zamýšlené fungování systému ve formě časových logických vzorců. V takovém případě je přirozený přístup k ověření kontrola modelu, který spočívá v rozhodnutí, zda model systému vyhovuje logickým vlastnostem či nikoli. CADP obsahuje nástroje pro kontrolu modelu pro výkonnou formu časové logiky, modální mu-kalkul, který je rozšířen o typované proměnné a výrazy, aby vyjádřil predikáty nad údaji obsaženými v modelu. Toto rozšíření poskytuje vlastnosti, které nelze vyjádřit ve standardním mu-kalkulu (například skutečnost, že hodnota dané proměnné se vždy zvyšuje po jakékoli cestě provedení).

I když jsou tyto techniky efektivní a automatizované, jejich hlavním omezením je problém exploze stavu, ke kterému dochází, když jsou modely příliš velké, aby se vešly do paměti počítače. CADP poskytuje softwarové technologie pro manipulaci s modely dvěma doplňkovými způsoby:

  • Malé modely lze explicitně reprezentovat uložením všech jejich stavů a ​​přechodů do paměti (vyčerpávající ověření);
  • Větší modely jsou zastoupeny implicitně zkoumáním pouze stavů modelů a přechodů potřebných k ověření (ověřování za běhu).

Jazyky a techniky kompilace

Přesná specifikace spolehlivých a složitých systémů vyžaduje jazyk, který je spustitelný (pro enumerativní ověření) a má formální sémantiku (aby nedocházelo k jazykovým nejasnostem, které by mohly vést k rozdílům v interpretaci mezi designéry a implementátory). Formální sémantika je rovněž nutná, pokud je nutné stanovit správnost nekonečného systému; toto nelze provést pomocí výčtu technik, protože se zabývají pouze konečnými abstrakcemi, takže je nutné je provést pomocí technik dokazování teorémů, které platí pouze pro jazyky s formální sémantikou.

CADP působí na a LOTOS popis systému. LOTOS je mezinárodní standard pro popis protokolu (ISO / IEC standard 8807: 1989), který kombinuje koncepty procesních algeber (zejména CCS a CSP a algebraické abstraktní datové typy. LOTOS tedy může popsat jak asynchronní souběžné procesy, tak složité datové struktury.

Program LOTOS byl silně revidován v roce 2001, což vedlo k vydání E-LOTOS (Enhanced-Lotos, norma ISO / IEC 15437: 2001), který se snaží poskytnout větší expresivitu (například zavedením kvantitativního času k popisu systémů s reálnými časová omezení) společně s lepší uživatelskou přívětivostí.

Existuje několik nástrojů pro převod popisů v jiných procesních kalkulích nebo mezilehlém formátu do systému LOTOS, takže nástroje CADP lze poté použít k ověření.

Licencování a instalace

CADP je bezplatně distribuován na univerzity a do veřejných výzkumných středisek. Uživatelé v průmyslu mohou získat zkušební licenci pro nekomerční použití po omezenou dobu, po které je vyžadována plná licence. Chcete-li požádat o kopii CADP, vyplňte registrační formulář na adrese.[3] Po podepsání licenční smlouvy obdržíte podrobnosti o tom, jak stáhnout a nainstalovat CADP.

Souhrn nástrojů

Sada nástrojů obsahuje několik nástrojů:

  • CAESAR.ADT[4] je překladač, který překládá LOTOS abstraktní datové typy do typů C a funkcí C. Překlad zahrnuje techniky kompilace porovnávání vzorů a automatické rozpoznávání obvyklých typů (celá čísla, výčty, n-tice atd.), Které jsou implementovány optimálně.
  • CAESAR[5] je překladač, který převádí procesy LOTOS buď do kódu C (pro účely rychlých prototypů a testování), nebo do konečných grafů (pro ověření). Překlad se provádí pomocí několika mezikroků, mezi nimiž je konstrukce Petriho sítě rozšířené o typované proměnné, funkce pro zpracování dat a atomové přechody.
  • OTEVŘENO / CAESAR[6] je obecné softwarové prostředí pro vývoj nástrojů, které prozkoumávají grafy za běhu (například nástroje pro simulaci, ověřování a generování testů). Tyto nástroje lze vyvíjet nezávisle na jakémkoli konkrétním jazyce na vysoké úrovni. V tomto ohledu hraje OPEN / CAESAR ústřední roli v CADP propojením jazykově orientovaných nástrojů s nástroji orientovanými na modely. OPEN / CAESAR se skládá ze sady 16 knihoven kódů s jejich programovacími rozhraními, například:
    • Caesar_Hash, který obsahuje několik hashovacích funkcí
    • Caesar_Solve, který řeší booleovské systémy rovnic za běhu
    • Caesar_Stack, který implementuje komíny pro průzkum vyhledávání do hloubky
    • Caesar_Table, který zpracovává tabulky stavů, přechodů, štítků atd.

V prostředí OPEN / CAESAR byla vyvinuta řada nástrojů:

    • BISIMULATOR, který kontroluje ekvivalence a předobjednávky bisimulace
    • CUNCTATOR, který provádí simulaci ustáleného stavu za chodu
    • DETERMINÁTOR, který eliminuje stochastický nedeterminismus v normálních, pravděpodobnostních nebo stochastických systémech
    • DISTRIBUTOR, který generuje graf dosažitelných stavů pomocí několika strojů
    • EVALUATOR, který vyhodnocuje pravidelné vzorce mu-kalkulu bez střídání
    • EXECUTOR, který provádí náhodné provádění kódu
    • VYSTAVOVATEL, který hledá spouštěcí sekvence odpovídající danému regulárnímu výrazu
    • GENERATOR, který sestrojuje graf dosažitelných stavů
    • PREDICTOR, který předpovídá proveditelnost analýzy dosažitelnosti,
    • PROJEKTOR, který počítá abstrakce komunikujících systémů
    • REDUKTOR, který konstruuje a minimalizuje graf dosažitelných stavů modulo různých vztahů ekvivalence
    • SIMULATOR, X-SIMULATOR a OCIS, které umožňují interaktivní simulaci
    • TERMINÁTOR, který hledá zablokované stavy
  • BCG (Binary Coded Graphs) je formát souboru pro ukládání velmi velkých grafů na disk (s využitím efektivních kompresních technik) i softwarové prostředí pro manipulaci s tímto formátem, včetně dělení grafů pro distribuované zpracování. BCG také hraje klíčovou roli v CADP, protože mnoho nástrojů spoléhá na tento formát pro své vstupy / výstupy. Prostředí BCG se skládá z různých knihoven s jejich programovacími rozhraními a několika nástrojů, včetně:
    • BCG_DRAW, který vytváří dvojrozměrný pohled na graf,
    • BCG_EDIT, který umožňuje interaktivně upravovat rozložení grafu vytvořeného programem Bcg_Draw
    • BCG_GRAPH, který generuje různé formy prakticky užitečných grafů
    • BCG_INFO, který zobrazuje různé statistické informace o grafu
    • BCG_IO, který provádí převody mezi BCG a mnoha dalšími formáty grafů
    • BCG_LABELS, který skryje a / nebo přejmenuje (pomocí regulárních výrazů) popisky přechodu grafu
    • BCG_MERGE, který shromažďuje fragmenty grafů získané z distribuované konstrukce grafů
    • BCG_MIN, který minimalizuje graf modulo silné nebo větvící ekvivalence (a může se také zabývat pravděpodobnostními a stochastickými systémy)
    • BCG_STEADY, která provádí ustálenou numerickou analýzu (rozšířených) kontinuálních Markovových řetězců
    • BCG_TRANSIENT, který provádí přechodnou numerickou analýzu (rozšířených) Markovových řetězců v nepřetržitém čase
    • PBG_CP, který kopíruje rozdělený graf BCG
    • PBG_INFO, který zobrazuje informace o rozděleném grafu BCG
    • PBG_MV, který pohybuje rozděleným BCG grafem
    • PBG_RM, který odstraní rozdělený graf BCG
    • XTL (eXecutable Temporal Language), což je funkční jazyk na vysoké úrovni pro programování algoritmů průzkumu na grafech BCG. XTL poskytuje primitiva pro zpracování stavů, přechodů, štítků, nástupnických a předchůdcových funkcí atd. Například lze definovat rekurzivní funkce na množinách stavů, které umožňují specifikovat v XTL vyhodnocení a generování diagnostiky algoritmy pevných bodů pro obvyklé časové logiky (jako jako HML,[7] CTL,[8] ACTL,[9] atd.).

Spojení mezi explicitními modely (například grafy BCG) a implicitními modely (zkoumanými za běhu) zajišťují kompilátory kompatibilní s OPEN / CAESAR, včetně:

    • CAESAR.OPEN, pro modely vyjádřené jako popisy LOTOS
    • BCG.OPEN, pro modely představované jako grafy BCG
    • EXP.OPEN, pro modely vyjádřené jako komunikující automaty
    • FSP.OPEN, pro modely vyjádřené jako popisy FSP
    • LNT.OPEN, pro modely vyjádřené jako popisy LNT
    • SEQ.OPEN, pro modely představované jako sady trasování provádění

Sada nástrojů CADP také obsahuje další nástroje, jako jsou ALDEBARAN a TGV (Test Generation based on Verification) vyvinuté laboratoří Verimag (Grenoble) a projektovým týmem Vertecs společnosti INRIA Rennes.

Nástroje CADP jsou dobře integrované a lze k nim snadno přistupovat pomocí grafického rozhraní EUCALYPTUS nebo SVL[10] skriptovací jazyk. EUCALYPTUS i SVL poskytují uživatelům snadný a jednotný přístup k nástrojům CADP automatickým převodem formátu souboru, kdykoli je to potřeba, a poskytnutím vhodných možností příkazového řádku při vyvolání nástrojů.

Viz také

  • SYNTAX generátor překladače (slouží k sestavení mnoha CADP překladatelé a překladatelé)

Reference

  1. ^ Garavel H, Lang F, Mateescu R, Serwe W: CADP 2011: Sada nástrojů pro konstrukci a analýzu distribuovaných procesů International Journal on Software Tools for Technology Transfer (STTT), 15 (2): 89-107, duben 2013
  2. ^ ISO 8807, Jazyk specifikace časových objednávek
  3. ^ Online formulář žádosti CADP. Cadp.inria.fr (2011-08-30). Citováno 2014-06-16.
  4. ^ H. Garavel. Kompilace abstraktních datových typů LOTOS, v Sborník z 2. mezinárodní konference o technikách formálního popisu FORTE'89 (Vancouver B.C., Kanada), S. T. Vuong (editor), North-Holland, prosinec 1989, s. 147–162.
  5. ^ H. Garavel, J. Sifakis. Kompilace a ověření specifikací systému LOTOS, v Sborník z 10. mezinárodního sympózia o specifikaci, testování a ověřování protokolů (Ottawa, Kanada), L. Logrippo, R. L. Probert, H. Ural (redakce), North-Holland, IFIP, červen 1990, s. 379–394.
  6. ^ H. Garavel. OPEN / CÆSAR: Otevřená softwarová architektura pro ověřování, simulaci a testování, Ve sborníku z první mezinárodní konference o nástrojích a algoritmech pro konstrukci a analýzu systémů TACAS'98 (Lisabon, Portugalsko), Berlín, B. Steffen (editor), Přednášky z informatiky, Plná verze k dispozici jako Zpráva o výzkumu Inria RR-3352 Springer Verlag, březen 1998, roč. 1384, s. 68–84.
  7. ^ M. Hennessy, R. Milner. Algebraické zákony pro nedeterminismus a souběžnost, v: Deník ACM1985, sv. 32, s. 137–161.
  8. ^ E. M. Clarke, E. A. Emerson, A. P. Sistla. Automatické ověřování souběžných systémů konečných stavů pomocí specifikací časové logiky, v: Transakce ACM v programovacích jazycích a systémech, Duben 1986, roč. 8, č. 2, s. 244–263.
  9. ^ R. De Nicola, F. W. Vaandrager. Akce versus stavová logika pro přechodové systémy, Přednášky z informatikySpringer Verlag, 1990, sv. 469, s. 407–419.
  10. ^ H. Garavel, F. Lang.SVL: skriptovací jazyk pro kompoziční ověření, v: Sborník z 21. mezinárodní konference IFIP WG 6.1 o formálních technikách pro síťové a distribuované systémy FORTE'2001 (Ostrov Cheju, Korea), M. Kim, B. Chin, S. Kang, D. Lee (redaktoři), plná verze k dispozici jako Zpráva o výzkumu Inria RR-4223, Kluwer Academic Publishers, IFIP, srpen 2001, s. 377–392.

externí odkazy