Interpolation-Based Multi-core Bounded Model Checking of HSTM Designs

Kun Liu, Xiaozhen Zhang, Weiqiang Kong, Gang Hou, Masahiko Watanabe, Akira Fukuda

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Bounded model checking, an effective way to reduce the state space, plays a significant role in verifying the reliability of a system. By combining bounded model checking and interpolation sequence, the verification of the properties out of some certain boundary can be completed. However, the introduction of interpolation-sequence increases the complexity of the model encoding and then affects the overall performance of a model checker. In order to alleviate the problem, we propose interpolation-based multi-core bounded model checking technology. Decomposing large problems into small ones, multicore parallel solutions can effectively shorten the elapsed time of problem processing. According to the conditional predicates, the paths in the model are divided into path clusters, and the interpolation sequence is used to determine if there is no counterexample path in each path cluster. Based on the nature of fixpoint in the path cluster, we propose a path cluster pruning algorithm in order to reduce the scale of the state space to be searched, which contributes to improving the efficiency. In this paper, we also present two optimization methods: incremental encoding and verification hypothesis. We have implemented the algorithms in the verification of the Hierarchical State Transition Matrix (HSTM) model design, and the experimental results have shown that our method have significantly increase the credibility of the verification results.

Original languageEnglish
Title of host publicationProceedings - 2019 6th International Conference on Dependable Systems and Their Applications, DSA 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages25-36
Number of pages12
ISBN (Electronic)9781728160573
DOIs
Publication statusPublished - Jan 2020
Event6th International Conference on Dependable Systems and Their Applications, DSA 2019 - Harbin, China
Duration: Jan 3 2020Jan 6 2020

Publication series

NameProceedings - 2019 6th International Conference on Dependable Systems and Their Applications, DSA 2019

Conference

Conference6th International Conference on Dependable Systems and Their Applications, DSA 2019
CountryChina
CityHarbin
Period1/3/201/6/20

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Computer Science Applications
  • Information Systems
  • Information Systems and Management
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Interpolation-Based Multi-core Bounded Model Checking of HSTM Designs'. Together they form a unique fingerprint.

Cite this