J 2012

Verification of Systems with Degradation

BARNAT, Jiří; Ivana ČERNÁ a Jana TŮMOVÁ

Základní údaje

Originální název

Verification of Systems with Degradation

Autoři

Vydání

Computing and Informatics, 2012, 1335-9150

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Slovensko

Utajení

není předmětem státního či obchodního tajemství

Impakt faktor

Impact factor: 0.254

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/12:00057864

Organizační jednotka

Fakulta informatiky

UT WoS

Klíčová slova anglicky

Systems with degradation; Linear Temporal Logic; Quantitative model checking; Automata-based approach to verification; Timed automata
Změněno: 11. 4. 2013 12:56, RNDr. Jana Tůmová, Ph.D.

Anotace

V originále

We 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.

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ů
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