Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction
| Název česky | Modelování a formální analýza komponentových systémů z pohledu interakce mezi komponentami |
|---|---|
| Autoři | |
| Rok publikování | 2008 |
| Druh | Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.) |
| Fakulta / Pracoviště MU | |
| Citace | |
| Popis | Vývoj bezchybných komponentových systémů je velice obtížný úkol z důvodu vysoké pravděpodobnosti konfliktů ve vzájemné interakci komponent, které jsou z principu komponentového vývoje vytvořeny nezávisle na sobě. Vzhledem k rostoucím možnostem výpočetní techniky se pro řešení tohoto úkolu nabízí využití automatizovaných formálních metod. Před samotnou aplikací formálních metod je však třeba vytvořit model studovaného systému, pro který je třeba nalézt vhodný modelovací formalismus. Ten by měl být dostatečně přesný, aby zachytil všechny podstatné informace pro formální analýzu. Na druhou stranu ale musí abstrahovat od těch aspektů, které nejsou pro analýzu nezbytné a mohly by vést k nepřiměřenému nárůstu velikosti modelu. Cílem této práce je přispět k vývoji v oblasti formální analýzy komponentových systémů ve dvou směrech. Prvním je navržení formálního přístupu k modelování interakcí mezi komponentami. Pro tyto účely navrhujeme nový modelovací jazyk, nazvaný Component-Interaction automaty. Kromě definice jazyka a diskuze jeho možných kompozičních operátorů, je velká část práce věnována jeho aplikaci na modelování interakcí mezi komponentami. Práce provádí celým modelovacím procesem a poté se věnuje zachycení nejrůznějších aspektů reálných systémů, jakými jsou interní stavy komponent, práce s výjimkami, modelování asynchronní komunikace, nebo konstrukce a destrukce instancí komponent. Druhým směrem studovaným v této práci je formální analýza vytvořených modelů. Na základě formalismu Component-Interaction automatů a definované ekvivalenci mezi jednotlivými modely, práce navrhuje přístup k vývoji komponentových systémů garantující správnost z podstaty použitých kroků vývoje. Konkrétně studujeme takové situace v procesu vývoje, kdy může ověření vzájemného vztahu artefaktů na různých úrovních předejít vzniku chyb v systému. Takovými situacemi jsou například integrace nezávisle vytvořených komponent, nebo výměna existujících komponent za nové. |
| Související projekty: |