Abstrakt
Pro rozsáhlé systémy softwarových komponent je značnou výhodou ověřit jejich správnost ještě před reálným nasazením. Abychom dosáhli důvěryhodné kompozice, je chování komponent formálně popsáno a správnost jejich použití je ověřeno vzhledem k chybám v komunikaci.
Naneštěstí množství stavů, které je nutné vytvořit během ověřování, běžně roste exponenciálné s velikostí popisu systému, což často způsobuje nepraktické nároky na čas ověřování a množství dostupné paměti. V této práci prezentujeme několik technik, které mají za úkol nepříznivý růs počtu stavů omezit. Nejdříve rozšíříme specifikační jazyk o kontrukce, které umožní při stejné vyjadřovací síle generovat menší model.
Dále redukujeme počet stavů automatickou modifikací specifikace aniž bychom ovlivňovali výslednou korektnost. Popisujeme také novou metodu rozložení výpočetní úlohy na více strojů a metodu konstrukce reprezentantů.