Verification of Systems with Degradation

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2012
Type Article in Periodical
Magazine / Source Computing and Informatics
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords Systems with degradation; Linear Temporal Logic; Quantitative model checking; Automata-based approach to verification; Timed automata
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.