data structures and software dependability

• home

• contact

• members

• teaching

• research

• publications

• software

• events

Certifiable logic programmable controllers

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

Objectives

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.

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

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. [ pdf ] [ BibTeX ]
• [Spranger01]
  Jochen Spranger:
  Symbolic LTL verification of Petri nets;
  PhD thesis, BTU Cottbus, Dep. of CS, December 2001. [ pdf ] [ 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 ]

Slides

• [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.