| Identifikační kód | RIV/00216224:14330/14:00073420 |
|---|
| Název v anglickém jazyce | Temporal Verification of Simulink Diagrams |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2014 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 3 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792)
Petr Bauch (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5736935)
Vojtěch Havel (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3095673) |
|---|
| Popis výsledku v anglickém jazyce | 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 formulaein the bit-vector theory and compared using satisfiability modulo theory solvers, scale well to arbitrary (though still bounded) range of input variables. |
|---|
| Klíčová slova oddělená středníkem | temporal verification; ltl model checking; simulink diagrams |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|