Attributes | Values |
---|
rdf:type
| |
rdfs:seeAlso
| |
Description
| - Quality assurance processes based mainly on humans are not suitable for development of current extensive hardware and software systems. Application of automatic verification tools is a promising solution. Research in the area of automatic formal verification is the aim of the proposed project. More precisely, the proposer intends to focus on the following three areas. Properties of temporal logics and aplication of these properties to development of new or improvement of the current verificationalgorithms properties of formalisms for modeling infinite-state systems - their expressive power and decidability of basic verification problems for the corresponding classes of infinite-state systems progressive directions in software verifications - inparticular verification of properties related to dynamic memory allocation and applications of verification techiques to common programming languages. The output of this research project will be papers in international journals and papers at (en)
- Procesy ověřování a garance kvality založené převážně na práci lidí nejsou vhodné pro vývoj dnešních rozsáhlých hardwarových a softwarových systémů. Perspektivním řešením je použití automatizovaných nástrojů pro formální verifikaci systémů. A právě výzkum v oblasti automatické formální verifikace je tématem předkládaného projektu. Navrhovatel se chce konkrétně zaměřit na tři oblasti: vlastnosti temporálních logik a využití těchto vlastností při konstrukci nových a vylepšení stávajících verifikačních algoritmů, vlastnosti formalismů pro popis nekonečně stavových systémů - jejich vyjadřovací síla a rozhodnutelnost základních verifikačních problémů pro odpovídající třídy nekonečně stavových systémů, progresivní směry ve verifikaci softwaru - zejména verifikace vlastností souvisejících s dynamicky alokovanou pamětí a aplikace verifikačních technik na běžné programovací jazyky. Výstupem projektu budou publikace v mezinárodních časopisech a na mezinárodních konferencích a
|
Title
| - Formal verification: algorithms, properties of modelling formalisms and temporal logics (en)
- Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
|
skos:notation
| |
http://linked.open...avai/cep/aktivita
| |
http://linked.open...kovaStatniPodpora
| |
http://linked.open...ep/celkoveNaklady
| |
http://linked.open...datumDodatniDoRIV
| |
http://linked.open...i/cep/druhSouteze
| |
http://linked.open...ep/duvernostUdaju
| |
http://linked.open.../cep/fazeProjektu
| |
http://linked.open...ai/cep/hlavniObor
| |
http://linked.open...hodnoceniProjektu
| |
http://linked.open...vai/cep/kategorie
| |
http://linked.open.../cep/klicovaSlova
| - formal verification; model checking; infinite systems; temporal logics (en)
|
http://linked.open...ep/partnetrHlavni
| |
http://linked.open...inujicichPrijemcu
| |
http://linked.open...cep/pocetPrijemcu
| |
http://linked.open...ocetSpoluPrijemcu
| |
http://linked.open.../pocetVysledkuRIV
| |
http://linked.open...enychVysledkuVRIV
| |
http://linked.open...lneniVMinulemRoce
| |
http://linked.open.../prideleniPodpory
| |
http://linked.open...iciPoslednihoRoku
| |
http://linked.open...atUdajeProjZameru
| |
http://linked.open.../vavai/cep/soutez
| |
http://linked.open...usZobrazovaneFaze
| |
http://linked.open...ai/cep/typPojektu
| |
http://linked.open...ep/ukonceniReseni
| |
http://linked.open...ep/zahajeniReseni
| |
http://linked.open...jektu+dodavatelem
| - Cílem projektu bylo dosažení výsledků ve třech oblastech: vlastnosti temporálních logik, vlastnosti nekonečně-stavových systémů a progresivní směry ve verifikaci softwaru. V první oblasti jsme nejprve dokázali, že fragment LTL obsahující modality eventually a always lze transformovat do LTL formulí velmi speciálního tvaru, pro které pak byl navrhnut algoritmus pro model checking wPRS systémů (p (cs)
- The aim of the project was to achieve results in three areas: properties of temporal logics, properties of infinite-state systems, and progressive directions in software verification. In the first area, we proved that the LTL fragment with modalities eventually and always can be transformed to LTL formulae of a special form and we presented an algorithm for model checking of such formulae and wP (en)
|
http://linked.open...tniCyklusProjektu
| |
http://linked.open.../cep/klicoveSlovo
| - formal verification
- infinite systems
- model checking
|
is http://linked.open...vavai/riv/projekt
of | |
is http://linked.open...vavai/cep/projekt
of | |