Formal Verification of Industrial Controllers: with or without a Plant model?
José Machado, Bruno Denis, Jean-Jacques Lesage · HAL (Le Centre pour la Communication Scientifique Directe) · 2006
The use of a plant model for formal verification of industrial controllers makes the formal verification tasks more realistic, because any industrial system is always composed by a controller and a plant. Therefore, if the plant model is not used, there is a part of the system that is not considered. However, if there are some cases where the use of a plant model becomes the formal verification results more realistic and robust there are other cases where it nor always happens. In this paper there are indicated which are the circumstances where it is useful to use, or not, a plant model on formal verification tasks, using model-checking techniques.