Realistická aplikace formálních metod v komponentových systémech
Cíle projektu
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 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 prostředí.
Klíčová slova
formal verificationbehavior descriptionsoftware componentscomponent systems
Veřejná podpora
Poskytovatel
Akademie věd České republiky
Program
Informační společnost (Národní program výzkumu)
Veřejná soutěž
Informační společnost 2 (SAV02005-IS)
Hlavní účastníci
—
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
1ET400300504
Alternativní jazyk
Název projektu anglicky
Realistic application of formal methods in component systems
Anotace anglicky
The project supports component-based application development by combining components with formal behavior description and by designing tools for automated checking of the architecture of applications composed of components with formal behavior description. The project aims to design and implement a functional prototype of a platform for formal verification of component application properties, and to propose and test methods for verification of software components and component applications using this platform. The platform will be open to the emerging methods of formal verification and code analysis, and used to test the suitability and applicability of these methods, especially with respect to model checking. The work on the formal verification methods will focus on identifying approaches to make the existing verification tools more efficient, especially in a distributed environment.
Vědní obory
Kategorie VaV
NV - Neprůmyslový výzkum (aplikovaný výzkum s výjimkou průmyslového)
CEP - hlavní obor
IN - Informatika
CEP - vedlejší obor
JC - Počítačový hardware a software
CEP - další vedlejší obor
—
OECD FORD - odpovídající obory
(dle převodníku)10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
20206 - Computer hardware and architecture
Hodnocení dokončeného projektu
Hodnocení poskytovatelem
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Zhodnocení výsledků projektu
Projekt navrhl, prototypově implementoval a na případových studiích ověřil nové metody formální verifikace vlastností modelů a implementace komponentových systémů založené na formalismech interagujících automatů a rozšířených protokolů chování.
Termíny řešení
Zahájení řešení
1. 1. 2005
Ukončení řešení
31. 12. 2009
Poslední stav řešení
U - Ukončený projekt
Poslední uvolnění podpory
11. 3. 2009
Dodání dat do CEP
Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP10-AV0-1E-U/01:1
Datum dodání záznamu
15. 4. 2010
Finance
Celkové uznané náklady
12 881 tis. Kč
Výše podpory ze státního rozpočtu
12 881 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Základní informace
Uznané náklady
12 881 tis. Kč
Statní podpora
12 881 tis. Kč
100%
Poskytovatel
Akademie věd České republiky
CEP
IN - Informatika
Doba řešení
01. 01. 2005 - 31. 12. 2009