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

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

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

V originále

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

Přiložené soubory

paper_46.pdf

Požádat o autorskou verzi souboru