Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00089030" target="_blank" >RIV/00216224:14330/16:00089030 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1007/s11219-014-9259-x" target="_blank" >http://dx.doi.org/10.1007/s11219-014-9259-x</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s11219-014-9259-x" target="_blank" >10.1007/s11219-014-9259-x</a>

Result language

angličtina

Original language name

Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories

Original language description

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.

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

IN - Informatics

OECD FORD branch

—

Project

<a href="/en/project/7H13001" target="_blank" >7H13001: Critical System Engineering Acceleration</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2016

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Software Quality Journal

ISSN

0963-9314

e-ISSN

—

Volume of the periodical

24

Issue of the periodical within the volume

1

Country of publishing house

US - UNITED STATES

Number of pages

27

Pages from-to

37-63

UT code for WoS article

000369006200004

EID of the result in the Scopus database

—