RIV/00216224:14330/12:00057864 - Verification of Systems with Degradation (2012)

Údaje o výsledku
Identifikační kódRIV/00216224:14330/12:00057864
Název v původním jazyceVerification of Systems with Degradation
DruhJ - Článek v odborném periodiku
Jazykeng - angličtina
OborIN - Informatika
Rok uplatnění2012
Kód důvěrnosti údajůS - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
Počet výskytů výsledku2
Údaje z Hodnocení výsledků výzkumných organizací 2014
Výsledek byl hodnocen v Pilíři I
Rozsah vyřazení výsledkuTento výskyt výsledku není vyřazen
Zařazení výsledku v hodnoceníJimp - Článek v impaktovaném časopise evidovaném ve Web of Science
Skupina oboru v hodnocení04 - Technické a informatické vědy
Konkrétní způsob(y) hodnocení výsledkuVýsledek hodnocený již v předchozím hodnocení, body se přebírají
Bodové ohodnocení11,037
Faktor korekce90,8 %
Body (upravené podle přílohy č. 8 Metodiky)10,024
Rozdělení výsledku mezi předkladatele
OrganizaceVýzkumná organizace?PodílBodyBody (upravené podle přílohy č. 8 Metodiky)
Masarykova univerzita / Fakulta informatikyano100,0 %11,03710,024
Tvůrci výsledku
Počet tvůrců celkem3
Počet domácích tvůrců3
TvůrceBarnat Jiří (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 5692792)
TvůrceČerná Ivana (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 2361132)
TvůrceTůmová Jana (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 4293738)
Údaje blíže specifikující výsledek
Popis v původním jazyceWe focus on systems that naturally incorporate a degrading quality, such as electronic devices with degrading electric charge or broadcasting networks with decreasing power or quality of a transmitted signal. For such systems, we introduce an extension of linear temporal logic (Linear Temporal Logic with Degradation Constraints, or DLTL for short) that provides a user-friendly formalism for specifying properties involving quantitative requirements on the level of degradation. We investigate possibility of translating DLTL verification problem for systems with degradation into previously solved MITL verification problem for timed automata, and we show that through the translation, DLTL model checking problem can be solved with limited, yet arbitrary, precision. For a specific subclass of DLTL formulas, we present a full precision verification technique based on translation of DLTL formulas into a specification formalism called Buchi Automata with Degradation Constraints (BADCs) developed earlier.
Klíčová slovaSystems with degradation; Linear Temporal Logic; Quantitative model checking; Automata-based approach to verification; Timed automata
Kód UT ISI000307127500003
Název periodkaComputing and Informatics
Rozsah stran507-530
ISSN1335-9150
Svazek periodika31
Číslo periodika v rámci uvedeného svazku3
Stát vydavatele periodikaSK - Slovenská republika
Počet stran výsledku24
Údaje o tomto záznamu o výsledku
PředkladatelMasarykova univerzita / Fakulta informatiky
DodavatelMSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT)
Rok sběru2013
Systémové označení dodávky datRIV13-MSM-14330___/02:2
SpecifikaceRIV/00216224:14330/12:00057864!RIV13-MSM-14330___
Kontrolní kód[04F472D20691]
Další výskyty tohoto výsledku od stejného předkladatele
Dodáno GA ČR v roce 2013Záznam s identifikačním kódem RIV/00216224:14330/12:00057864 v dodávce dat RIV13-GA0-14330___/02:2
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
ProjektGAP202/11/0312 - Vývoj a verifikace softwarových komponent v zapouzdřených systémech (2011-2013, GA0/GA)
ProjektGD102/09/H042 - Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů (2009-2012, GA0/GD)
ProjektLH11065 - Řízení a ověřování vlastností komplexních hybridních systémů (2011-2014, MSM/LH)