Structural reasoning in proving system correctness

Formal validation of the industrial systems requires new ways to make this process more user-friendly. The usability of formal methods can be increased by employing new analysis techniques. This paper describes a method to evaluate system state spaces. The system state space or reachability graph is considered as a finite structure that can be manipulated to provide more readable result. Therefore the structural reasoner tool also presented in the paper simplifies an analysis of the system. It can be seen as an addition to the traditional methods such as a model-checking.