The more critical systems embed software, the more it is questionable to use classical methods such as fault trees, event trees or stochastic simulation on Petri nets to assess their reliability. This means that in the near future, reliability and dependability analyses will have to integrate more and more techniques developped by the so-called "formal methods" communauty. The aim of this paper is to provide practitioners with a tutorial introduction to model checking, one of the most used techniques in the formal methods framwork.
展开▼