Assurance of some system reliability characteristics in formal design verification

ABSTRACT. Abstract--In this paper we consider two ways of using both formal-logical models based on Model Checking and Markov probabilistic models for semi-automatic verification of robustness to Soft Errors of a target design, and assurance of these properties as well. One of this approach to verification is well-known Probabilistic Model Checking while another is suggested recently a combination of traditional Model Checking with a two–dimensional Markov chain. A comparison of computational complexities of these approaches shows that combination of Model Checking formal verification with analysis of fault-tolerant property could reduce overall design cost, what can increase considerably the formal verification tools effectiveness.