Realistic application of formal methods in component systems
Project goals
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.
Keywords
formal verificationbehavior descriptionsoftware componentscomponent systems
Public support
Provider
Academy of Sciences of the Czech Republic
Programme
Information society (National programme of research)
Call for proposals
Informační společnost 2 (SAV02005-IS)
Main participants
—
Contest type
VS - Public tender
Contract ID
1ET400300504
Alternative language
Project name in Czech
Realistická aplikace formálních metod v komponentových systémech
Annotation in Czech
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í.
Scientific branches
R&D category
NV - Nonindustrial research (Applied research excluded Industrial research)
CEP classification - main branch
IN - Informatics
CEP - secondary branch
JC - Computer hardware and software
CEP - another secondary branch
—
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
20206 - Computer hardware and architecture
Completed project evaluation
Provider evaluation
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Project results evaluation
The project has proposed, implemented as a prototype, and on case studies tested multiple new methods of formal verification of component systems (both model and implementation), based on the formalisms of interacting automata and behavior protocols.
Solution timeline
Realization period - beginning
Jan 1, 2005
Realization period - end
Dec 31, 2009
Project status
U - Finished project
Latest support payment
Mar 11, 2009
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP10-AV0-1E-U/01:1
Data delivery date
Apr 15, 2010
Finance
Total approved costs
12,881 thou. CZK
Public financial support
12,881 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
12 881 CZK thou.
Public support
12 881 CZK thou.
100%
Provider
Academy of Sciences of the Czech Republic
CEP
IN - Informatics
Solution period
01. 01. 2005 - 31. 12. 2009