Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories

BAUCH, Petr, Vojtěch HAVEL a Jiří BARNAT. Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories. Software Quality Journal. Springer, 2016, roč. 24, č. 1, s. 37-63. ISSN 0963-9314. Dostupné z: https://dx.doi.org/10.1007/s11219-014-9259-x.

Základní údaje

• Originální název: Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories
• Autoři: BAUCH, Petr (203 Česká republika, domácí), Vojtěch HAVEL (203 Česká republika, domácí) a Jiří BARNAT (203 Česká republika, domácí).
• Vydání: Software Quality Journal, Springer, 2016, 0963-9314.

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Článek v odborném periodiku
• 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í
• Impakt faktor: Impact factor: 1.816
• Kód RIV: RIV/00216224:14330/16:00089030
• Organizační jednotka: Fakulta informatiky
• Doi: http://dx.doi.org/10.1007/s11219-014-9259-x
• UT WoS: 000369006200004
• Klíčová slova anglicky: formal verification; model checking; circuit analysis; satisfiability modulo theories
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

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 non-determinism 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 formulas in the bit-vector theory and compared using satisfiability modulo theory solvers, scale well to arbitrary (though still bounded) range of input variables. To leverage the combined strengths of explicit and symbolic representations, we have designed a hybrid representation which we showed to outperform both pure representations. Thus the proposed method allows complete automatic verification without the need to limit the non-determinism of input. Moreover, the principle underlying the hybrid representation entails inferring knowledge about the system under verification, which the developers did not explicitly include in the system, and which can significantly accelerate the verification process.

Návaznosti

• 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

• 7H13001, projekt VaV: Název: Critical System Engineering Acceleration (Akronym: CRYSTAL (MSMT))

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Critical System Engineering Acceleration