Optimization of checking the feasibility of transitions when verifying formal models

A.V. Kolchin

Abstract


Transitions feasibility analysis becomes a significant part of operation time of verification tools for formal models of programs, which control flow is expressed implicitly. This paper describes a new method of model checking performance improvement. The main idea is a localization of a transition’s unsatisfiability reason in some state and it’s usage for the satisfiability analysis in subsequent states.

Keywords


Верификация

References


Holzmann G. The model checker SPIN // IEEE transactions on software engineering. – 1997. – Vol. 23. – N 5. – P. 279–295.

Holzmann G., Peled D. An improvement in formal verification // FORTE 1994 Conference. – 1994. – P. 197–211.

Zhang Y., Rodriguez E., Zheng H., Myers C. A Behavioral Analysis Approach for Efficient Partial Order Reduction // In proc. of the 13th IEEE International Symposium on High-Assurance Systems Engineering. – 2011. – P. 49–56.

Jussila T. On Bounded Model Checking of Asynchronous Systems // Doctoral Thesis. Helsinki University of Technology, Laboratory for Theoretical Computer Science. Research report A97. – 2005. – P. 136.

Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST // International Journal Software Tools Technology Transfer. – 2007. – N 9. – P. 505–525.

Zheng H. Compositional reachability analysis for efficient modular verification of asynchronous designs // IEEE Trans. on CAD of Integrated Circuits and Systems. – 2010. – Vol. 29. – P. 329–340.

Колчин А.В. Автоматический метод динамического построения абстракций состояний формальной модели // Кибернетика и системный анализ. – 2010. – № 4. – С. 70–90.

Летичевский А., Капитонова Ю., Волков В. и др. Спецификация систем с помощью базовых протоколов // Кибернетика и системный анализ. – 2005. – № 4. – С. 3–21.

Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. – М.: Мир, 1979. – С. 536.

Letichevsky A., Kapitonova J., Konozenko S. Computations in APS // Theoretical Computer Science. – 1993. – Vol. 119. – P. 145–171.


Refbacks

  • There are currently no refbacks.