Informace o projektu
Realistická aplikace formálních metod v komponentových systémech
- Kód projektu
- 1ET400300504
- Období řešení
- 1/2005 - 12/2009
- Investor / Programový rámec / typ projektu
-
Akademie věd ČR
- Informační společnost (Národní program výzkumu)
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Klíčová slova
- formální verifikace, popisy chování, softwarové komponenty, komponentové systémy
- Spolupracující organizace
-
Ústav informatiky AV ČR, v. v. i.
- Odpovědná osoba prof. Ing. František Plášil, DrSc.
- Odpovědná osoba prof. Ing. Petr Tůma, Dr.
Projekt podporuje využití komponent jako sílící trend ve vývoji aplikací, a to kombinováním komponent s formálním popisem chování a návrhem nástrojů schopných provést automaticky kontrolu architektury aplikací složených z komponent s formálním popisem chování. Projekt si klade za cíl navrhnout a realizovat platformu pro podporu formální verifikace vlastností komponentových aplikací na úrovni funkčního prototypu a s použitím této platformy navrhnout metody pro verifikaci softwarových komponent a komponentových aplikací a ověřit uplatnění těchto metod. Vytvořená platforma bude otevřená vznikajícím metodám pro formální verifikaci a analýzu kódu a použita pro ověřování vhodnosti a použitelnosti těchto metod, zejména technice model a checking. Práce na metodách formální verifikace se budou soustředit na identifikaci postupů, které umožní výrazné zefektivnění stávajících nástrojů pro automatickou verifikaci, zejména v distribuovaném protředí.
Výsledky
Předpokládané výsledky projektu jsou směřovány do oboru softwarového inženýrství, zejména konstrukce komponentových aplikací. Perspektivní technologie komponent si již našla průmyslové uplatnění, navrhovaný projekt spojuje tuto technologii s technikou model checking (ověřování modelů) do otevřeného systému abstrahujícího od konkrétního komponentového modelu a konkrétního formalismu. Projekt poskytne platformu nutnou pro převod výsledků do praxe, dosud ztížený odbornou náročností použití formálních metod a nedůvěrou producentů software v komponenty jako takové a především ve formální metody. Nezanedbatelným přínosem projektu pro převod výsledků do praxe budou výsledky ověřování navržených formálních metod na vyvinuté platformě, stejně jako předávání získaných poznatků studentům.
Publikace
Počet publikací: 29
2008
-
Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems
Proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08), rok: 2008
-
Component-Interaction Automata Approach (CoIn)
The Common Component Modeling Example: Comparing Software Component Models, rok: 2008, počet stran: 31 s.
-
Formal verification of systems with an unlimited number of components
IET Software journal, rok: 2008, ročník: Volume 2, vydání: Isuue 6
-
Model Checking of Control-User Component-Based Parametrised Systems
Rok: 2008, druh: Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
-
Model Checking of Control-User Component-Based Parametrised Systems
Lecture Notes in Computer Science 5282, rok: 2008
-
Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction
Rok: 2008, druh: Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
-
Partial Order Reduction for State/Event LTL
Rok: 2008
-
Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking
Tools and Algorithms for the Construction and Analysis of Systems, rok: 2008
-
The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems
Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08), rok: 2008
2007
-
Component Substitutability via Equivalencies of Component-Interaction Automata
Electronic Notes in Theoretical Computer Science, rok: 2007, ročník: 182, vydání: 1