Temporal Verification of Simulink Diagrams

BARNAT, Jiří, Petr BAUCH a Vojtěch HAVEL. Temporal Verification of Simulink Diagrams. Online. In P. J. Clarke et al. 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.

Základní údaje

Originální název

Temporal Verification of Simulink Diagrams

Autoři

BARNAT, Jiří (203 Česká republika, domácí), Petr BAUCH (203 Česká republika, domácí) a Vojtěch HAVEL (203 Česká republika, domácí)

Vydání

Miami, Proceedings of HASE 2014, od s. 81-88, 8 s. 2014

Nakladatel

IEEE Computer Society

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

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

Forma vydání

elektronická verze "online"

Kód RIV

RIV/00216224:14330/14:00073420

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4799-3465-2

DOI

http://dx.doi.org/10.1109/HASE.2014.20

UT WoS

000351728000011

Klíčová slova anglicky

temporal verification; ltl model checking; simulink diagrams

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.

---

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
MUNI/A/0760/2012, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0765/2013, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU) Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0855/2013, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty