• česky
  • english
Přejít na obsah | Přejít na menu

Informační systém výzkumu, experimentálního vývoje a inovací
výzkum, vývoj a inovace podporované z veřejných prostředků ČR

    • Poskytovatelé podpory ve výzkumu, vývoji a inovacích (RPO)
    • Programy výzkumu, vývoje a inovací (RPG)
    • Subjekty ve výzkumu, vývoji a inovacích (RPR)
  • Veřejné soutěže ve výzkumu, vývoji a inovacích (VES)
  • Projekty výzkumu, vývoje a inovací (CEP)
  • Výzkumné záměry (CEZ)
  • Výsledky výzkumu, vývoje a inovací (RIV)

1ET408050503 - Techniky automatické verifikace a validace softwarových a hardwarových systémů (2005-2009, AV0/1E)

Údaje o projektu
Identifikační kód1ET408050503
Důvěrnost údajůS - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
Název v původním jazyceTechniky automatické verifikace a validace softwarových a hardwarových systémů
PoskytovatelAV0 - Akademie věd České republiky (AV ČR)
Program1E - Informační společnost (Národní program výzkumu) (2004-2009)
Kategorie VaVNV - Aplikovaný výzkum s výjimkou průmyslového výzkumu (tzv. "neprůmyslový výzkum")
Hlavní oborIN - Informatika
Vedlejší oborJC - Počítačový hardware a software
Další vedlejší oborBA - Obecná matematika
Zahájení řešení1.1.2005
Ukončení řešení31.12.2009
Datum posledního uvolnění účelové podpory11.3.2009
Číslo smlouvy1ET408050503
Poslední stav řešeníU - Ukončený projekt, tj. jednoletý nebo víceletý projekt, který skončil v předcházejícím roce, v příslušném roce sběru dat jsou dodány údaje vztahující se k jeho ukončení
Finance projektu
Období20052006200720082009celkem
Výše podpory ze státního rozpočtu2 120 tis. Kč2 135 tis. Kč1 935 tis. Kč1 935 tis. Kč1 829 tis. Kč9 954 tis. Kč
Celkové uznané náklady2 120 tis. Kč2 135 tis. Kč1 935 tis. Kč1 935 tis. Kč1 829 tis. Kč9 954 tis. Kč
Typskutečně čerpanéskutečně čerpanéskutečně čerpanéskutečně čerpanéskutečně čerpané
Druh soutěžeVS - Veřejná soutěž ve výzkumu a vývoji
Veřejná soutěž ve výzkumu, vývoji a inovacíchSAV02005-IS - Veřejná soutěž (AV0/1E)
Cíle řešení v původním jazyceHlavním cílem projektu je vytvoření teoreticko-metodologického zázemí počítačem podporované a automatické verifikace rozsáhlých softwarových a hardwarových systémů. Projekt si klade za úkol podpořit vývoj metodologií, technologií a nástrojů softwarového inženýrství v oblasti technik automatické verifikace. Projekt přispěje k výzkumu směřujícímu k rozvoji poznatků o technologiích pro realistické modelování rozsáhlých systémů, včetně systémů reálného času a pravděpodobnostních systémů, specielně s ohledem na bezpečnost jejich provozu. Cílem je navrhnout efektivní implementace těchto modelů a na nich založených metodologiích pro efektivní verifikaci. Projekt se zaměří na zapouzdřené, distribuované a paralelní systémy. Vzhledem k výpočetní náročnosti a rozsáhlosti procesu verifikace je cílem navrhnout metodologie využívající v maximální míře i nové možnosti výpočetních technologií, např. ve smyslu paralelního a distribuovaného počítaní a v hierarchickém přístupu k paměti.
Klíčová slova v anglickém jazycecomputer aided and automatic verification; theory and technology of modelling of large systems; methodology of software engineering; embedded systems; parallel and distributed systems; real time systems
Hodnocení výsledkůV - Vynikající výsledky (s mezinárodním významem apod.). Zároveň byly splněny cíle a předpokládané výsledky uvedené ve smlouvě / rozhodnutí o poskytnutí podpory.
Zhodnocení výsledků řešení českyParalelní algoritmy pro základní podúlohy při automatizované verifikaci (detekce akceptujících cyklů v orientovaných grafech, rozklad na silně souvislé komponenty ap.). Vývoj paralelního verifikačního nástroje DiVinE a jeho aplikace.
Rok dodání údajů do CEP2010
Systémové označení dodávky datCEP10-AV0-1E-U/01:1
Datum dodání záznamu15.4.2010
Účastníci projektu
Počet příjemců1
Počet dalších účastníků projektu0
Příjemce / Organizační jednotka garantující řešeníMasarykova univerzita / Fakulta informatiky
Řešitelprof. RNDr. Luboš Brim, CSc. (státní příslušnost: CZ - Česká republika; tel.: 549493647; fax: 549491070)
Finance účastníků projektu
Poznámka: Finance účastníků projektu jsou sledovány od roku 2007
Výše podpory ze státního rozpočtu
Účastník200720082009
Masarykova univerzita / Fakulta informatiky1 935 tis. Kč1 935 tis. Kč1 829 tis. Kč
Celkové uznané náklady
Účastník200720082009
Masarykova univerzita / Fakulta informatiky1 935 tis. Kč1 935 tis. Kč1 829 tis. Kč
Výsledky projektu v RIV
Počet výsledků v RIV96
Výsledek druhu JRIV/00216224:14330/12:00057076 - On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties (2012)
Výsledek druhu JRIV/00216224:14330/11:00049494 - Distributed Algorithms for SCC Decomposition (2011)
Výsledek druhu JRIV/00216224:14330/11:00049402 - Flash memory efficient LTL model checking (2011)
Výsledek druhu JRIV/00216224:14330/10:00040530 - Scalable shared memory LTL model checking (2010)
Výsledek druhu DRIV/00216224:14330/09:00028695 - A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties (2009)
Výsledek druhu RRIV/00216224:14330/09:00028602 - BioDiVinE (2009)
Výsledek druhu DRIV/00216224:14330/09:00028618 - BioDiVinE: A Framework for Parallel Analysis of Biological Models (2009)
Výsledek druhu DRIV/00216224:14330/09:00028658 - Can Flash Memory Help in Model Checking? (2009)
Výsledek druhu DRIV/00216224:14330/09:00028497 - Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete (2009)
Výsledek druhu DRIV/00216224:14330/09:00028696 - Cluster-Based I/O-Efficient LTL Model Checking (2009)
Výsledek druhu DRIV/00216224:14330/09:00028617 - Computational Analysis of Large-Scale Multi-Affine ODE Models (2009)
Výsledek druhu DRIV/00216224:14330/09:00028692 - CUDA Accelerated LTL Model Checking (2009)
Výsledek druhu RRIV/00216224:14330/09:00028810 - DiVinE 2.0 (2009)
Výsledek druhu DRIV/00216224:14330/09:00028659 - DiVinE 2.0: High-Performance Model Checking (2009)
Výsledek druhu RRIV/00216224:14330/09:00028808 - DiVinE Cuda (2009)
Výsledek druhu JRIV/00216224:14330/09:00028691 - DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking (2009)
Výsledek druhu ORIV/00216224:14330/09:00028656 - On Computational Analysis of Large ODE Models (2009)
Výsledek druhu DRIV/00216224:14330/09:00028439 - On Decidability of LTL+Past Model Checking for Process Rewrite Systems (2009)
Výsledek druhu DRIV/00216224:14330/09:00028468 - Partial Order Reduction for State/Event LTL (2009)
Výsledek druhu JRIV/00216224:14330/09:00028490 - Reachability is decidable for weakly extended process rewrite systems (2009)
Výsledek druhu DRIV/00216224:14330/08:00024388 - A Case Study in Parallel Verification of Component-Based Systems (2008)
Výsledek druhu JRIV/00216224:14330/08:00024171 - A Case Study in Parallel Verification of Component-Based Systems (2008)
Výsledek druhu DRIV/00216224:14330/08:00024304 - Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems (2008)
Výsledek druhu DRIV/00216224:14330/08:00024294 - The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems (2008)
Výsledek druhu CRIV/00216224:14330/08:00024133 - Component-Interaction Automata Approach (CoIn) (2008)
Výsledek druhu RRIV/00216224:14330/08:00024473 - DiVinE Cluster (2008)
Výsledek druhu DRIV/00216224:14330/08:00024321 - DiVinE Multi-Core -- A Parallel LTL Model-Checker (2008)
Výsledek druhu ORIV/00216224:14330/08:00024337 - Estimating State Space Parameters (2008)
Výsledek druhu JRIV/00216224:14330/08:00024358 - Formal verification of systems with an unlimited number of components (2008)
Výsledek druhu DRIV/00216224:14330/08:00024175 - From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks (2008)
Výsledek druhu RRIV/00216224:14330/08:00024471 - GeNeSim: Genetic Network Simulator GUI (2008)
Výsledek druhu JRIV/00216224:14330/08:00024165 - Improved Distributed Algorithms for SCC Decomposition (2008)
Výsledek druhu DRIV/00216224:14330/09:00028657 - Local Quantitative LTL Model Checking (2009)
Výsledek druhu DRIV/00216224:14330/08:00024313 - Model Checking of Control-User Component-Based Parametrised Systems (2008)
Výsledek druhu ORIV/00216224:14330/08:00028409 - On Algorithmic Analysis of Biological Networks (2008)
Výsledek druhu DRIV/00216224:14330/08:00024143 - Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE (2008)
Výsledek druhu ARIV/00216224:14330/08:00024265 - Partial Order Reduction for State/Event LTL (2008)
Výsledek druhu JRIV/00216224:14330/08:00024164 - Petri Nets Are Less Expressive Than State-Extended PA (2008)
Výsledek druhu RRIV/00216224:14330/08:00024418 - ProbDiVinE-MC (2008)
Výsledek druhu DRIV/00216224:14330/08:00024323 - ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems (2008)
Výsledek druhu DRIV/00216224:14330/08:00024177 - Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking (2008)
Výsledek druhu DRIV/00216224:14330/08:00024282 - Semi-external LTL Model Checking (2008)
Výsledek druhu JRIV/00216224:14330/08:00024166 - Shared Hash Tables in Parallel Model Checking (2008)
Výsledek druhu DRIV/00216224:14330/08:00024322 - Squeeze All the Power Out of Your Hardware to Verify Your Software! (2008)
Výsledek druhu JRIV/00216224:14330/07:00019439 - Component Substitutability via Equivalencies of Component-Interaction Automata (2007)
Výsledek druhu RRIV/00216224:14330/07:00019614 - DiVinE Multi-Core (2007)
Výsledek druhu DRIV/00216224:14330/07:00019481 - Effective verification of systems with a dynamic number of components (2007)
Výsledek druhu ARIV/00216224:14330/07:00019613 - Formalisms and Tools for Design and Specification of Network Protocols (2007)
Výsledek druhu JRIV/00216224:14330/07:00019458 - Improved Distributed Algorithms for SCC Decomposition (2007)
Výsledek druhu DRIV/00216224:14330/07:00019426 - I/O Efficient Accepting Cycle Detection (2007)
Výsledek druhu DRIV/00216224:14330/07:00019356 - Model Checking Large Finite-State Systems and Beyond (2007)
Výsledek druhu ORIV/00216224:14330/07:00019467 - On Decidability of LTL+Past Model Checking for Process Rewrite Systems (2007)
Výsledek druhu DRIV/00216224:14330/07:00019374 - Parallel Algorithms for Finding SCCs in Implicitly Given Graphs (2007)
Výsledek druhu JRIV/00216224:14330/07:00019374 - Parallel Algorithms for Finding SCCs in Implicitly Given Graphs (2007)
Výsledek druhu ORIV/00216224:14330/07:00019480 - Parallel Analysis of Genetic Regulatory Networks (2007)
Výsledek druhu ARIV/00216224:14330/07:00019480 - Parallel Analysis of Genetic Regulatory Networks (2007)
Výsledek druhu DRIV/00216224:14330/07:00019460 - Parallel Model Checking and the FMICS-jETI Platform (2007)
Výsledek druhu RRIV/00216224:14330/07:00024472 - ProbDiVinE (2007)
Výsledek druhu DRIV/00216224:14330/07:00019472 - ProbDiVinE: A Parallel Qualitative LTL Model Checker (2007)
Výsledek druhu DRIV/00216224:14330/07:00019497 - Relaxed Cycle Condition Improves Partial Order Reduction (2007)
Výsledek druhu DRIV/00216224:14330/07:00019427 - Scalable Multi-core LTL Model-Checking (2007)
Výsledek druhu JRIV/00216224:14330/07:00019427 - Scalable Multi-core LTL Model-Checking (2007)
Výsledek druhu JRIV/00216224:14330/07:00019459 - Shared Hash Tables in Parallel Model Checking (2007)
Výsledek druhu DRIV/00216224:14330/07:00019329 - Verifying VHDL Designs with Multiple Clocks in SMV (2007)
Výsledek druhu DRIV/00216224:14330/06:00015346 - Architectural Interoperability Checking in Visual Coordination Networks (2006)
Výsledek druhu DRIV/00216224:14330/06:00015451 - Cluster-Based LTL Model Checking of Large Systems (2006)
Výsledek druhu JRIV/00216224:14330/06:00015451 - Cluster-Based LTL Model Checking of Large Systems (2006)
Výsledek druhu DRIV/00216224:14330/06:00015414 - Component Substitutability via Equivalencies of Component-Interaction Automata (2006)
Výsledek druhu JRIV/00216224:14330/06:00015452 - Distributed breadth-first search LTL model checking (2006)
Výsledek druhu DRIV/00216224:14330/06:00015450 - Distributed Qualitative LTL Model Checking of Markov Decision Processes (2006)
Výsledek druhu DRIV/00216224:14330/06:00015443 - DiVinE -- A Tool for Distributed Verification (2006)
Výsledek druhu JRIV/00216224:14330/06:00015443 - DiVinE -- A Tool for Distributed Verification (2006)
Výsledek druhu RRIV/00216224:14330/06:00024474 - DiVinE Library (2006)
Výsledek druhu DRIV/00216224:14330/06:00015311 - Formal Verification of a FIFO Component in Design of Network Monitoring Hardware (2006)
Výsledek druhu JRIV/00216224:14330/06:00015453 - How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors (2006)
Výsledek druhu JRIV/00216224:14330/06:00015466 - Model Checking of RegCTL (2006)
Výsledek druhu DRIV/00216224:14330/06:00015442 - On Combining Partial Order Reduction with Fairness Assumptions (2006)
Výsledek druhu DRIV/00216224:14330/06:00015417 - On Decidability of LTL Model Checking for Process Rewrite Systems (2006)
Výsledek druhu JRIV/00216224:14330/06:00015417 - On Decidability of LTL Model Checking for Process Rewrite Systems (2006)
Výsledek druhu ARIV/00216224:14330/06:00015439 - On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems (2006)
Výsledek druhu JRIV/00216224:14330/06:00015292 - Refining Undecidability Border of Weak Bisimilarity (2006)
Výsledek druhu DRIV/00216224:14330/06:00015292 - Refining Undecidability Border of Weak Bisimilarity. (2006)
Výsledek druhu DRIV/00216224:14330/06:00015335 - Routing and Level 2 Addressing in a Hardware Accelerator for Network Applications (2006)
Výsledek druhu DRIV/00216224:14330/06:00015369 - Test Input Generation for Java Containers using State Matching (2006)
Výsledek druhu ORIV/00216224:14330/06:00015476 - Weakly Extended Process Rewrite Systems (2006)
Výsledek druhu DRIV/00216224:14330/05:00012728 - Concrete Search with Abstract Matching and Refinement (2005)
Výsledek druhu ARIV/00216224:14330/05:00012922 - CRC64 Algorithm Analysis and Verification (2005)
Výsledek druhu JRIV/00216224:14330/05:00012729 - Deeper Connections between LTL and Alternating Automata (2005)
Výsledek druhu DRIV/00216224:14330/05:00012727 - Enhancing Random Walk State Space Exploration (2005)
Výsledek druhu WRIV/00216224:14330/05:00013425 - MTCoord 2005 1st International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (2005)
Výsledek druhu DRIV/00216224:14330/05:00012726 - On Sampled Semantics of Timed Systems (2005)
Výsledek druhu DRIV/00216224:14330/05:00012582 - Reachability of Hennessy - Milner properties for weakly extended PRS (2005)
Výsledek druhu JRIV/00216224:14330/05:00012582 - Reachability of Hennessy - Milner properties for weakly extended PRS (2005)
Výsledek druhu JRIV/00216224:14330/05:00012580 - Refining Undecidability Border of Weak Bisimilarity. (2005)
Výsledek druhu ARIV/00216224:14330/05:00012581 - Refining Undecidability Border of Weak Bisimilarity. (full version of INFINITY 2005 paper) (2005)
Výsledek druhu JRIV/00216224:14330/05:00012554 - The stuttering principle revisited (2005)
Tuto aplikaci pro Radu pro výzkum, vývoj a inovace provozuje Výpočetní a informační centrum Českého vysokého učení technického v Praze. Vyvíjí InfoScience Praha s.r.o.. Verze aplikace 1.6.15. Datové schéma ISVAV_WEB5_00305. Podpora uživatelů na e-mailové adrese podpora (zavináč) isvav (tečka) cz nebo telefonním čísle 224 234 797 (v pracovních dnech 8-16 hod.).