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

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

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

抄録

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.

本文言語英語
ホスト出版物のタイトルProceedings - 2019 6th International Conference on Dependable Systems and Their Applications, DSA 2019
出版社Institute of Electrical and Electronics Engineers Inc.
ページ25-36
ページ数12
ISBN(電子版)9781728160573
DOI
出版ステータス出版済み - 1 2020
イベント6th International Conference on Dependable Systems and Their Applications, DSA 2019 - Harbin, 中国
継続期間: 1 3 20201 6 2020

出版物シリーズ

名前Proceedings - 2019 6th International Conference on Dependable Systems and Their Applications, DSA 2019

会議

会議6th International Conference on Dependable Systems and Their Applications, DSA 2019
Country中国
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

フィンガープリント 「Interpolation-Based Multi-core Bounded Model Checking of HSTM Designs」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル