Formal Model-Based Development in Industrial Automation with Reactive Blocks

The use of standard IT equipment to control machines is becoming increasingly popular mostly due to lower costs. Further, trends and initiatives such as Industry 4.0 and smart factories accelerate the use of standard IT components by demanding interconnected controllers and factory equipment communicating with internet services. This development offers new possibilities to use existing software frameworks and software architectural approaches as well as development standards in industrial automation. The formal methods-based support, that already exists for standard IT platforms, can now be applied to industrial control devices as well. In this paper, we look into the application of our Reactive Blocks framework for industrial automation. Reactive Blocks comes with a well established formal semantics and verification approaches tied to it. We demonstrate the advantages of our methodology with an example.