data structures and software dependability

computer science department

brandenburg university of technology cottbus - senftenberg

Certifiable logic programmable controllers

latest update: March 23, 2019, at 02:12 PM


The goal of the project is the computer aided development of verifiable reliable controller software. A 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 Automation technology (Prof. Meier) of the Brandenburg Techn. Univ. of Cottbus.


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


PhD Theses

  • [Mertke03]
    Thomas Mertke:
    A Technical Language for Formal Safety Specification of Reactive Systems;
    PhD thesis, BTU Cottbus, Dep. of CS, October 2003. [ pdf ] [ BibTeX ]
  • [Deussen01]
    Peter Deussen:
    Analysis of concurrent systems by Process Automata;
    PhD thesis, BTU Cottbus, Dep. of CS, December 2001. [ BibTeX ]
  • [Spranger01]
    Jochen Spranger:
    Symbolic LTL verification of Petri nets;
    PhD thesis, BTU Cottbus, Dep. of CS, December 2001. [ BibTeX ]

Some papers

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


  • [H04.sld2]
    M Heiner:
    Modelchecking in der Automatisierungstechnik; Wie formal müssen formale Methoden sein?
    Talk, Software Forum Berlin-Brandenburg (invited talk), September 2004. [ pdf ] [ BibTeX ]

For more (including BTU reports, slides) see selected references.

… the end …

Any comments or questions are welcome. Please direct them to monika [period] heiner [snail] b-tu [period] de Privacy Policy