Další formáty:
BibTeX
LaTeX
RIS
@article{1075279,
author = {Barnat, Jiří and Černá, Ivana and Tůmová, Jana},
article_number = {3},
keywords = {Systems with degradation; Linear Temporal Logic; Quantitative model checking; Automata-based approach to verification; Timed automata},
language = {eng},
issn = {1335-9150},
journal = {Computing and Informatics},
title = {Verification of Systems with Degradation},
volume = {31},
year = {2012}
}
TY - JOUR
ID - 1075279
AU - Barnat, Jiří - Černá, Ivana - Tůmová, Jana
PY - 2012
TI - Verification of Systems with Degradation
JF - Computing and Informatics
VL - 31
IS - 3
SP - 507-530
EP - 507-530
SN - 13359150
KW - Systems with degradation
KW - Linear Temporal Logic
KW - Quantitative model checking
KW - Automata-based approach to verification
KW - Timed automata
N2 - 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.
ER -
BARNAT, Jiří, Ivana ČERNÁ a Jana TŮMOVÁ. Verification of Systems with Degradation. \textit{Computing and Informatics}. 2012, roč.~31, č.~3, s.~507-530. ISSN~1335-9150.
|
