Certifiable Logic Programmable Controllers

 Objectives

The goal of the project is the computer aided development of verifiable reliable controller software. A developmently development environment is in preparation. Essentially, this environment is a dedicated variant of a general framework for a Petri net bases workbench (compare our project 'Petri net workbench'). It should aid the whole development process of logic programmable controllers. The main task is to make a methodically and tool aided software technology available, which is dedicated to the special requirements and practice of the field. Therefore, it is more likely that there is a change of acceptance by controller programmers.

The components of the development environment will be collected into an integrated tool box for the engineering of certifiable controller software. Informal, semi-formal and graphical techniques in connection with in academically proved formal methods will be used.

Along this line, we had the DFG projects  "Me 1557/1-1 and 2", 1997 -  2001, in cooperation with the chair of Automatisierungstechnik (Prof. Meier) of the Brandenburg Techn. Univ. of Cottbus.

 Cooperation

• Prof. H. Meier, BTU Cottbus, Automatisierungstechnik, DFG projects "Me 1557/1-1 and 2", 1997 -  2001
• Prof. Dr. H.-M. Hanisch, Univ. Magdeburg, Automatisierungstechnik;

 Results

Ph. D. Theses

• Thomas Mertke:
  Zertifizierung von speicherprogrammierbaren Steuerungen, Oktober 2003.
• Peter Deussen:
  Analyse nebenläufiger Systeme mit Hilfe von Prozeßautomaten, Dezember 2001.
• Jochen Spranger:
  Symbolische LTL-Verifikation von Petrinetzen, Dezember 2001.

Some papers

• Deussen, P.:
  Partial Order Verification of Programmable Logic Controllers;
  Proc. 22nd International Conference, ICATPN 2001, Newcastle upon Tyne, UK, Juni 2001, LNCS 2075,  pp. 144 - 163.
• Heiner, M.; Menzel, Th.:
  Time-related Modelling of PLC Systems with Time-less Petri Nets;
  in Boel, R.; Stremerch, G. (eds.): Discrete Event Systems, Analysis and Control; Kluwer Academic Publishers 2000, pp. 275 - 282;
• Heiner, M.; Deussen, P.; Spranger, S.:
  A Case Study in Design and Verification of Manufacturing Systems with Hierarchical Petri Nets;
  Journal of Advanced Manufacturing Technology (1999), 15, pp. 139-152
• Heiner, M; Menzel, T.:
  A Petri Net Semantics for the PLC Language Instruction List;
  Proc. IEE Workshop on Discrete Event Systems (WODES '98), Cagliari/Italy, August 1998, pp. 161-165
• Heiner, M; Menzel, T.:
  Instruction List Verification Using a Petri Net Semantics;
  Proc. IEEE Int. Conf. on Systems, Man, and Cybernetics, San Diego, October 1998, pp. 716-721

Slides

• Heiner, M.:
  Modelchecking in der Automatisierungstechnik; Wie formal müssen formale Methoden sein?
  Software Forum Berlin-Brandenburg, September 2004, 20 p.
  

. . .  t h e  e n d  . . .