Top

Software Quality Journal

Published in:

01-03-2016

Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories

Authors: Petr Bauch, Vojtěch Havel, Jiří Barnat

Published in: Software Quality Journal | Issue 1/2016

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

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.

previous article Finding fault with fault injection: an empirical exploration of distortion in fault injection experiments

next article Toward high assurance software systems with adaptive fault management

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Translated into a full equation, the value of \(d_1\) in the next tick equals \(d^{\prime }_1=\min \{c_3,(\lnot sv_1\vee c_1>sd_{13}) ?c_4:d_1\}*{\texttt{int}} (\lnot sv_1 \vee c_1>sd_{13})\).

Code available at http://anna.fi.muni.cz/~xbauch/code.html#simulink.

Armando, A., Mantovani, J., & Platania, L. (2006). Bounded model checking of software using SMT solvers instead of SAT solvers. In SPIN, LNCS (Vol. 3925, pp. 146–162). New York: Springer. doi:10.1007/11691617_9.

Barnat, J., & Bauch, P. (2013). Control explicit-data symbolic model checking: An introduction. Technical report, Masaryk University. http://arxiv.org/abs/1303.7379.

Barnat, J., Beran, J., Brim, L., Kratochvíla, T., & Ročkai, P. (2012). Tool chain to support automated formal verification of avionics simulink designs. In FMICS, LNCS (Vol. 7437, pp. 78–92). New York: Springer. doi:10.1007/978-3-642-32469-7_6.

Barnat, J., Brim, L., Havel, V., Havlíček, J., Kriho, J., Lenčo, M., et al. (2013). DiVinE 3.0—Explicit-state model-checker for multithreaded C/C++ programs. In CAV (pp. 863–868). doi:10.1007/978-3-642-39799-8_60.

Barnat, J., Bauch, P., & Havel, V. (2014). Temporal verification of simulink diagrams. In Proceedings of the HASE (pp. 81–88). doi:10.1109/HASE.2014.20.

Barrett, C., Stump, A., & Tinelli, C. (2010). The SMT-LIB standard: Version 2.0. Technical report, The University of Iowa.

Biere, A., Cimatti, A., Clarke, E., Fujita, M., & Zhu, Y. (1999). Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of the DAC (pp. 317–320). ACM. doi:10.1145/309847.309942.

Bradley, A. (2011). SAT-based model checking without unrolling. In VMCAI (pp. 70–87). doi:10.1007/978-3-642-18275-4_7.

Braione, P., Denaro, G., Křena, B., & Pezzè, M. (2008). Verifying LTL properties of bytecode with symbolic execution. In Proceedings of the bytecode (pp. 1–14). Elsevier Science.

Bryant, R. (1991). On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Transactions on Computers, 40(2), 205–213. doi:10.1109/12.73590.MATHCrossRef

Bryant, R., & Chen, Y. A. (1995). Verification of arithmetic circuits with binary moment diagrams. In Proceedings of the DAC (pp. 535–541). doi:10.1145/217474.217583.

Bultan, T., Gerber, R., & Pugh, W. (1997). Symbolic model checking of infinite state systems using presburger arithmetic. In CAV, LNCS (Vol. 1254, pp. 400–411). New York: Springer. doi:10.1007/3-540-63166-6_39.

Bultan, T., Gerber, R., & League, C. (1998). Verifying systems with integer constraints and Boolean predicates: A composite approach. In Proceedings of the ISSTA (pp. 113–123). doi:10.1145/271771.271799.

Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., et al. (2002). NuSMV 2: An OpenSource tool for symbolic model checking. In CAV (pp. 241–268). doi:10.1007/3-540-45657-0_29.

Clarke, E., Emerson, E., & Sistla, A. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2), 244–263. doi:10.1145/5397.5399.MATHCrossRef

Cousot, P., & Cousot, R. (1977). Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the POPL (pp. 238–252). ACM. doi:10.1145/512950.512973.

de Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. In TACAS, LNCS (Vol. 4963, pp. 337–340). New York: Springer. doi:10.1007/978-3-540-78800-3_24.

Duret-Lutz, A., Klai, K., Poitrenaud, D., & Thierry-Mieg, Y. (2011). Self-loop aggregation product—A new hybrid approach to on-the-fly LTL model checking. In ATVA, LNCS (Vol. 6996, pp. 336–350). New York: Springer. doi:10.1007/978-3-642-24372-1_24.

Godefroid, P. (2003) Reasoning about abstract open systems with generalized module checking. In EMSOFT, LNCS (Vol. 2855, pp. 223–240). Springer. doi:10.1007/978-3-540-45212-6_15.

Hagen, G., & Tinelli, C. (2008). Scaling up the formal verification of lustre programs with SMT-based techniques. In Proceedings of the FMCAD (pp. 1–9). doi:10.1109/FMCAD.2008.ECP.19.

Halbwachs, N., Caspi, P., Raymond, P., & Pilaud, D. (1991). The synchronous data flow programming language LUSTRE. Proceedings of the IEEE, 79(9), 1305–1320. doi:10.1109/5.97300.CrossRef

Hungar, H., Grumberg, O., & Damm, W. (1995). What if model checking must be truly symbolic. In CHARME, LNCS (Vol. 987, pp. 1–20). New York: Springer. doi:10.1007/3-540-60385-9_1.

King, J. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7), 385–394. doi:10.1145/360248.360252.MATHCrossRef

Kroening, D., & Strichman, O. (2010). Decision procedures: An algorithmic point of view. New York: Springer.

Kupferman, O., & Vardi, M. (1996). Module checking. In CAV, LNCS (Vol. 1102, pp. 75–86). New York: Springer. doi:10.1007/3-540-61474-5_59.

Lin, H. (1996). Symbolic transition graph with assignment. In CONCUR, LNCS (Vol. 1119, pp. 50–65). New York: Springer. doi:10.1007/3-540-61604-7_47.

McMillan, K. (1992). Symbolic model checking. Ph.D. thesis, Carnegie Mellon University.

Meenakshi, B., Bhatnagar, A., & Roy, S. (2006). Tool for translating simulink models into input language of a model checker. In ICFEM, LNCS (Vol. 4260, pp. 606–620). New York: Springer. doi:10.1007/11901433_33.

Miller, S., Anderson, E., Wagner, L., Whalen, M., & Heimdahl, M. (2005). Formal verification of flight critical software. In Proceedings of the GNC (pp. 1–16).

Owicki, S., & Gries, D. (1976). An axiomatic proof technique for parallel programs I. Acta Informatica, 6, 319–340. doi:10.1007/BF00268134.MATHMathSciNetCrossRef

Sebastiani, R., Tonetta, S., & Vardi, M. (2005). Symbolic systems, explicit properties: On hybrid approaches for LTL symbolic model checking. In CAV, LNCS (Vol. 3576, pp. 100–246). New York: Springer. doi:10.1007/11513988_35.

Vardi, M., & Wolper, P. (1986). An automata—theoretic approach to automatic program verification. In Proceedings of the LICS (pp. 332–344). IEEE Computer Society Press.

Williams, P., Biere, A., Clarke, E., & Gupta, A. (2000). Combining decision diagrams and SAT procedures for efficient symbolic model checking. In CAV, LNCS (Vol. 1855, pp. 124–138). New York: Springer. doi:10.1007/10722167_13.

Wintersteiger, C., Hamadi, Y., & de Moura, L. (2013). Efficiently solving quantified bit-vector formulas. Formal Methods in System Design, 42(1), 3–23. doi:10.1007/s10703-012-0156-2.MATHCrossRef

Xie, T., Marinov, D., Schulte, W., & Notkin, D. (2005). Symstra: A framework for generating object-oriented unit tests using symbolic execution. In TACAS, LNCS (Vol. 3440, pp. 365–381). New York: Springer. doi:10.1007/978-3-540-31980-1_24.

Yang, Z., Wang, C., Gupta, A., & Ivančić, F. (2006). Mixed symbolic representations for model checking software programs. In Proceedings of the MEMOCODE (pp. 17–26). doi:10.1109/MEMCOD.2006.1695896.

Title: Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories
Authors: Petr Bauch
Vojtěch Havel
Jiří Barnat
Publication date: 01-03-2016
Publisher: Springer US
Published in: Software Quality Journal / Issue 1/2016
Print ISSN: 0963-9314
Electronic ISSN: 1573-1367
DOI: https://doi.org/10.1007/s11219-014-9259-x

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Other articles of this Issue 1/2016

Toward high assurance software systems with adaptive fault management

Special issue on High Assurance Systems Engineering

Assessing vulnerability exploitability risk using software properties

Normalizing variations in feature vector structure in keystroke dynamics authentication systems

Certifying a java type resolution function using program transformation, annotation, and reflection

Finding fault with fault injection: an empirical exploration of distortion in fault injection experiments

Premium Partner