Timed Automata Approach to Verification of Systems with Degradation

BARNAT, Jiří, Ivana ČERNÁ a Jana TŮMOVÁ. Timed Automata Approach to Verification of Systems with Degradation. In MEMICS 2011. LNCS 7119. Heidelberg: Springer, 2012, s. 84 - 93. ISBN 978-3-642-25928-9. Dostupné z: https://dx.doi.org/10.1007/978-3-642-25929-6_8.

Základní údaje

• Originální název: Timed Automata Approach to Verification of Systems with Degradation
• Autoři: BARNAT, Jiří (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, garant, domácí) a Jana TŮMOVÁ (203 Česká republika, domácí).
• Vydání: LNCS 7119. Heidelberg, MEMICS 2011, od s. 84 - 93, 10 s. 2012.
• Nakladatel: Springer

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Německo
• Utajení: není předmětem státního či obchodního tajemství
• Forma vydání: tištěná verze "print"
• Impakt faktor: Impact factor: 0.402 v roce 2005
• Kód RIV: RIV/00216224:14330/12:00057212
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-3-642-25928-9
• ISSN: 0302-9743
• Doi: http://dx.doi.org/10.1007/978-3-642-25929-6_8
• Klíčová slova anglicky: model checking; linear temporal properties with degradation
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

We focus on systems that naturally incorporate a degrad- ing 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 with quantitative constraints (Linear Temporal Logic with Degra- dation Constraints) that provides a user-friendly for- malism for specifying properties involving quantitative requirements on the level of degradation. The syntax of DLTL resembles syntax of Metric Interval Temporal Logic (MITL) designed for reasoning about timed systems. Thus, we investigate their relation and a possibility of translating DLTL verication problem for systems with degradation into previously solved MITL verication problem for timed automata. We show, that through the mentioned translation, the DLTL model checking problem can be solved with limited, yet arbitrary, precision.

Návaznosti

• GAP202/11/0312, projekt VaV: Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)

Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification

• GD102/09/H042, projekt VaV: Název: 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ů

Investor: Grantová agentura ČR, 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ů

• LH11065, projekt VaV: Název: Řízení a ověřování vlastností komplexních hybridních systémů (Akronym: Řízení a ověřování vlastností komplexních hybridní)

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Řízení a ověřování vlastností komplexních hybridních systémů

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

• MUNI/A/0914/2009, interní kód MU: Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty