Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1129340,
author = {Barnat, Jiří and Bauch, Petr and Havel, Vojtěch},
address = {Miami},
booktitle = {Proceedings of HASE 2014},
doi = {http://dx.doi.org/10.1109/HASE.2014.20},
editor = {P. J. Clarke et al.},
keywords = {temporal verification; ltl model checking; simulink diagrams},
howpublished = {elektronická verze "online"},
language = {eng},
location = {Miami},
isbn = {978-1-4799-3465-2},
pages = {81-88},
publisher = {IEEE Computer Society},
title = {Temporal Verification of Simulink Diagrams},
year = {2014}
}
TY - JOUR
ID - 1129340
AU - Barnat, Jiří - Bauch, Petr - Havel, Vojtěch
PY - 2014
TI - Temporal Verification of Simulink Diagrams
PB - IEEE Computer Society
CY - Miami
SN - 9781479934652
KW - temporal verification
KW - ltl model checking
KW - simulink diagrams
N2 - Automatic verification of programs and computer systems with input variables represents a significant and well-motivated challenge. The case of Simulink diagrams is especially difficult, because there the inputs are read iteratively and the number of input variables is in theory unbounded. We apply the techniques of explicit model checking to account for the temporal (control) aspects of verification and use set-based representation of data, thus handling both sources of nondeterminism present in the verification. Two different representations of sets are evaluated in scalability with respect to the range of input variables. Explicit (enumerating) sets are very fast for small ranges but fail to scale. Symbolic sets, represented as first-order formulae in the bit-vector theory and compared using satisfiability modulo theory solvers, scale well to arbitrary (though still bounded) range of input variables. Thus the proposed method allows complete automatic verification without the need to limit the nondeterminism of input.
ER -
BARNAT, Jiří, Petr BAUCH a Vojtěch HAVEL. Temporal Verification of Simulink Diagrams. Online. In P. J. Clarke et al. \textit{Proceedings of HASE 2014}. Miami: IEEE Computer Society, 2014, s.~81-88. ISBN~978-1-4799-3465-2. Dostupné z: https://dx.doi.org/10.1109/HASE.2014.20.
|
