GM_Diss_2006

Marsal, G.:
Evaluation of time performances of Ethernet-based Automation Systems by simulation of high-level Petri-Nets.

Dissertation, Technische Universität Kaiserslautern, Germany and Ecole Normale Supérieur Cachan, France, Dec. 11th, 2006.

Shaker-Verlag, Aachen, Aug. 2007, ISBN: 978-3-8322-6407-9

Abstract:

Today there is a standard for the implementation of programs on Programmahle Logic Controllers (PLCs). Furthermore there are method'> for the formal devefopment ofthese 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 offunctionality especially needed in safety critical applications (e.g. using model checking)- However, there are a Iot of existing PLC programs that have been implemented in proprietary languages before a standard existed and even today formal rnethods are scarcely used during design. This work outlines a re-engineering approach based on the formalization of PLC programs. The PLC program modules aremodeledas Finite State Macllines (FSMs). These FSMs are able to communjcate with each other to describe the cornplete dynamic ofthe 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 ofits structure is identitied as an important intermediate step in this process. It is shown bow XML and corresponding technologies can be used for the formalization, visuali.zation, 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 fiir 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 Funkttonalität der Programme nachzuweisen. Letzteres ist insbesondere for sicherheitskritische Anwendungen unerlässlich. Leider gibt es jedoch eine ganze Reihe bestehender SPSProgramme die implementiert '11-'Urden, noch bevor der Standard existierte und selbst heute werden viele Programme noch ohne die Unterstützungformaler Methodiken entwo!fen. Im Rahmen dieser Arbeit wird ein Re-Engineering Ansatz vorgestellt, welcher auf der Formalisierung von SPSProgrammen beruht. Hierfiir 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 fiir den weiteren Systembearbeitungs- und -analyseprozess verwendet werden. Die Transformation des SPS-Programms in ein vom Hersteller unabhängiges Format stellt ebenso wie die Visu.alisierung der Programmstruktur einen wichtigen Schritt des Re-Engineering-Prozesses dar. In der Arbeit wird gezeigt, wie XML und die zugehörigen Techno/ogien für die Formalisiet'Ung, Visualisierung, Re-Implementierung und Softwarequalitätsmessung vorhandener SPS-Programme verwendet werden können.