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
2007
-
Effective verification of systems with a dynamic number of components
Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, rok: 2007
-
Subject-observer specification with component-interaction automata
Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, rok: 2007
2006
-
Component Placement in Distributed Environment w.r.t. Component Interaction
Proceedings of the 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06), rok: 2006
-
Component Substitutability via Equivalencies of Component-Interaction Automata
Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'06), rok: 2006
-
Component-Interaction Automata as a Verification-Oriented Component-Based System Specification
Software engineering notes : an informal newsletter of the Special Interest Committee on Software Engineering, rok: 2006, ročník: 31, vydání: 2
-
Component-Interaction Automata Modelling Language
Rok: 2006, druh: Prezentace v oblasti VaV (AV tvorba, WEB aplikace apod.)
-
Formal Analysis of Component-Based Systems in View of Comp. Interactions
Proceedings of the International Research Training Groups Workshop 2006, rok: 2006
2005
-
Component-Interaction Automata as a Verification-Oriented Component-Based System Specification
Proceedings of SAVCBS 2005, rok: 2005
-
Component-Interaction Automata for Specification and Verification of Component Interactions
IFM 2005 Doctoral Symposium on Integrated Formal Methods, rok: 2005