Úvod

Vývoj informatiky a výpočetní techniky a její stále častější nasazování v praxi v různých odvětvích průmyslu i služeb přináší četné aplikace neustále složitějších hardwarových i softwarových systémů. Většina těchto systémů má charakter souběžných systémů, jež jsou tvořeny často z velkého počtu vzájemně spolupracujících komponent běžících paralelně.

Souběžnost přináší exponenciální nárůst počtu všech možných běhů systému, které jsou dány různými souběhy paralelních komponent. Klasické techniky testování a ladění sekvenčních programů jsou pro souběžné systémy z tohoto důvodu prakticky nepoužitelné. Pro účely analýzy a formální verifikace souběžných systémů byla vyvinuta řada matematických technik, jež souhrnně nazýváme formálními metodami.

Verifikační techniky

jsou formální metody umožňující provést důkaz úplné nebo částečné správnosti systémů, zejména ověření zda implementace odpovídá specifikaci systému.

Mezi verifikační metody patří zejména testování ekvivalence (equivalence checking), ověřování modelů (model checking) a systémy dokazování vět (therem proving). Pro souběžné systémy byla navržena řada algoritmů pro automatizovanou verifikaci pomocí těchto metod. Ve vztahu k této práci uveďme zejména The Concurrency Workbench [], [].

Specifikační jazyk

je formální jazyk pro popis systémů. Pro různé třídy souběžných systémů existují specifikační jazyky přizpůsobené jejich specifickým vlastnostem. Abychom mohli systém verifikovat, musíme jej nejprve formálně specifikovat pomocí vhodného specifikačního jazyka.

Mezi specifikační jazyky řadíme algebry procesů (CCS [], CSP []) nebo Petriho sítě []. Pro praktickou specifikaci jsou často používány jazyky vyšší úrovně jako např. LOTOS [] nebo SDL [] vycházející z těchto matematických formalizmů. Ke specifikačním jazykům řadíme také různé logiky (modální a temporální logiky []) pro popis vlastností souběžných systémů.

Koordinační jazyk

je nástroj pro popis koordinačních vztahů mezi jednotlivými komponentami souběžného systému. Koordinační vztahy jsou vztahy definující vzájemnou interakci komponent systému. Interakcí rozumíme zejména komunikaci mezi jednotlivými částmi systému nebo jejich synchronizaci. []

Určitou nevýhodou těchto specifikačních formalizmů je jejich nesnadné praktické použití. Specifikace a popis systémů v těchto formalizmech vyžaduje jistý cvik a hlubší teoretické znalosti.

V oblasti softwarového inženýrství jsou hojně používanými specifikačními prostředky vývojové diagramy řízení a toku dat, které slouží zejména pro strukturní analýzu systémů []. Grafické formalizmy pro popis souběžných systémů vycházejí z těchto diagramů.

Rozšířený formální grafický nástroj pro popis systémů představují Petriho sítě. Jejich vlastnosti však nevyhovují požadavkům pro specifikaci rozsáhlých systémů. V této práci se zabýváme jazyky orientovanými na hierarchický a modulární popis systémů. O Petriho sítích se zmíníme proto jen ve stručnosti.

 
• Cíl a členění diplomové práce