Nowadays, formal methods are used in various areas for the verification of programs or for code generation from models in order to increase the quality of software and to reduce costs. However, there are still fields in which formal methods have not been widely adopted, despite the large set of possible benefits offered. This is the case for the area of programmable logic controllers (PLC). This article aims to evaluate the potential of formal methods in the context of PLC development. For this purpose, the general concepts of formal methods are first introduced and then transferred to the PLC area, resulting in an engineering-oriented description of the technology that is based on common concepts from PLC development. Based on this description, PLC professionals with varying degrees of experience were interviewed for their perspective on the topic and to identify possible use cases within the PLC domain. The survey results indicate the technology's high potential in the PLC area, either as a tool to directly support the developer or as a key element within a model-based systems engineering toolchain. The evaluation of the survey results is performed with the aid of a demo application that communicates with the Totally Integrated Automation Portal from Siemens and generates programs via Fastsynth, a model-based open source code generator. Benchmarks based on an industry-related PLC project show satisfactory synthesis times and a successful integration into the workflow of a PLC developer.

翻译：目前,在核查程序或从模型生成代码的各个领域都采用了正式方法,以便提高软件质量和降低成本,然而,仍有一些领域尚未广泛采用正式方法,尽管提供了大量可能的好处,如可编程逻辑控制器(PLC)领域的情况。本条款旨在评估在PLC开发过程中正式方法的潜力。为此,首先引入了正式方法的一般概念,然后将其转移到PLC领域,从而根据PLC开发的共同概念,对技术进行面向工程的描述。根据这一描述,对具有不同程度经验的PLC专业人员进行了访谈,以了解他们对这一问题的看法,并查明PLC领域可能使用的案例。调查结果表明,在PLC开发过程中,无论是作为直接支持开发者的一个工具,还是作为基于模型的系统工程工具链中的一个关键要素,在与Siemens开发的完全综合自动化的PLCF门户网站上,对基于Siemens的演示应用软件进行了侧重。通过快速合成时间,将一个基于软件集成源的计算机化、一个基于快速合成LCCS的计算机软件的软件版本,并制作一个完整的综合模型集成一个完整的版本。