Formal methods for higher reliability of the industrial automation

Industrial communication plays an important role in industrial measurement and control and particularly in process automation due to trend of decentralization of control systems. Process automation generally includes many areas of engineering (HW, SW, mechanical, chemical...) therefore close cooperation between them is necessary. But generally engineers from different branches use different descriptions and analyzing tools. Even the same areas of engineering use different description tools. The contribution show one of the possible ways how to solve this problem-using formal method. This methodology is demonstrated on a railway model. Model represents a typical system of logic control with voltage inputs and outputs, two different physical interfaces and serial communication subsystems and two control systems. Control architecture is designed as a fault tolerant system, what is common in process automation. Process variables are measured and controlled by both control systems (Masters). Two applications run inside both master. They ensure basic information exchange between appropriate master and slave station. This information exchange is based on developed protocol FTCP (fault tolerant control protocol) providing correct behaviour of the system if unexpected event is occurred-e.g. disjunction of the control bus, change of the control signal due to EMI, failing of the control element due to unexpected design error etc.