Formal Methods-Based Optimization of Dataflow Models with Translation to Synchronous Models

Graphical dataflow models are widely used for industrial control system implementation and are accepted by users with different backgrounds due to their intuitive visualization of the dataflow. As real-world applications have evolved, the complexity of these diagrams has increased, posing a challenge in the verification and maintenance of software models. In this paper, we argue that the perceived complexity of real-world applications can be simplified and transformed into formal models for reuse in software engineering or formal verification. To overcome the limitations of previous research on optimizing graphical dataflow models in an industrial context, we identify potentially optimizable submodels and optimize them, leaving the non-modifiable components unchanged. The optimized software model is then reconstructed and optionally translated into formal models for reuse or verification purposes. The paper describes the identification of submodels in real-world applications and demonstrates the need for configurability of the optimization. We present an open-source-based implementation using graphical dataflow models of programmable logic controllers and demonstrate the impact of our optimization approach using real-world applications from the literature and vendor-provided examples. The results help to reduce the complexity of existing dataflow models and to reuse existing real-world applications as formal software models.