Temporal Verification of Simulink Diagrams

BARNAT, Jiří, Petr BAUCH and Vojtěch HAVEL. Temporal Verification of Simulink Diagrams. Online. In P. J. Clarke et al. Proceedings of HASE 2014. Miami: IEEE Computer Society, 2014, p. 81-88. ISBN 978-1-4799-3465-2. Available from: https://dx.doi.org/10.1109/HASE.2014.20.

Basic information

Original name

Temporal Verification of Simulink Diagrams

Authors

BARNAT, Jiří (203 Czech Republic, belonging to the institution), Petr BAUCH (203 Czech Republic, belonging to the institution) and Vojtěch HAVEL (203 Czech Republic, belonging to the institution)

Edition

Miami, Proceedings of HASE 2014, p. 81-88, 8 pp. 2014

Publisher

IEEE Computer Society

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

Publication form

electronic version available online

RIV identification code

RIV/00216224:14330/14:00073420

Organization unit

Faculty of Informatics

ISBN

978-1-4799-3465-2

DOI

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

UT WoS

000351728000011

Keywords in English

temporal verification; ltl model checking; simulink diagrams

Tags

core_B, firank_B

Tags

International impact, Reviewed

---

Abstract

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.

---

Links

GAP202/11/0312, research and development project	Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems) Investor: Czech Science Foundation
MUNI/A/0760/2012, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Acronym: FI MAV II.) Investor: Masaryk University, Category A
MUNI/A/0765/2013, interní kód MU	Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU) Investor: Masaryk University, Category A
MUNI/A/0855/2013, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.) Investor: Masaryk University, Category A