MBY_Diss_2006

Bani Younis, Mohammed:
Re-Engineering Approach for PLC Programs based on Formal Methods.

Dissertation, Technische Universität Kaiserslautern, Kaiserslautern, Germany, Sept. 1st, 2006

Shaker-Verlag, Aachen, Nov. 2006, ISBN: 978-3-8322-5674-6

Abstract:

Today there is a standard for the implementation of programs on Programmable Logic Controllers (PLCs). Furthermore there are methods for the formal development of these programs. The standard allows the interchange of algorithms (e.g. if a new hardware should be used) and the formal methods allow the rigid proof of functionality especially needed in safety critical applications (e.g. using model checking). However, there are a lot of existing PLC programs that have been implemented in proprietary languages before a standard existed and even today formal methods are scarcely used during design. This work outlines a re-engineering approach based on the formalization of PLC programs. The PLC program modules are modeled as Finite State Machines (FSMs). These FSMs are able to communicate with each other to describe the complete dynamic of the PLC system. The resulting formal model can serve as a basis for editing and analyzing the system. The transformation of PLC programs into a vendor independent format and the visualization of its structure is identified as an important intermediate step in this process. It is shown how XML and corresponding technologies can be used for the formalization, visualization,
re-implementation, and software measurement of existing PLC programs.

Kurzfassung:

Für die Implementierung von Speicherprogrammierbaren Steuerungen (SPS) existiert heute ein Standard. Darüberhinaus gibt es eine ganze Reihe formaler Entwicklungsmethodiken für SPSProgramme. Während der SPS-Standard den Austausch von Algorithmen ermöglicht (z.B., wenn eine neue Hardware zum Einsatz kommen soll), stellt die Anwendung formaler Methoden die Möglichkeit dar, die Funktionalität der Programme nachzuweisen. Letzteres ist insbesondere für sicherheitskritische Anwendungen unerlässlich. Leider gibt es jedoch eine ganze Reihe bestehender SPSProgramme die implementiert wurden, noch bevor der Standard existierte und selbst heute werden
viele Programme noch ohne die Unterstützung formaler Methodiken entworfen. Im Rahmen dieser Arbeit wird ein Re-Engineering Ansatz vorgestellt, welcher auf der Formalisierung von SPSProgrammen beruht. Hierfür werden die SPS-Programmbausteine zunächst auf Basis von Automaten (Finite State Machines, FSM) modelliert. Diese FSMs kommunizieren miteinander um die vollständige Dynamik des SPS-Systems abzubilden. Das so entstehende formale Modell kann als Basis für den weiteren Systembearbeitungs- und -analyseprozess verwendet werden. Die Transformation des SPS-Programms in ein vom Hersteller unabhängiges Format stellt ebenso wie die Visualisierung
der Programmstruktur einen wichtigen Schritt des Re-Engineering-Prozesses dar. In der Arbeit wird gezeigt, wie XML und die zugehörigen Technologien für die Formalisierung, Visualisierung, Re-Implementierung und Softwarequalitätsmessung vorhandener SPS-Programme verwendet werden können.