Prof. Dr. habil. Henning Dierks

 

1 Publications (with abstracts)

[OD08]

E.-R. Olderog and H. Dierks. Real-Time Systems - Formal Specification and Automatic Verification. Cambridge University Press, 2008. ISBN 978-0-521-88333-7. For more information see: http://csd.informatik.uni-oldenburg.de/rt-book/.
[ bib ]

[Die05]

H. Dierks. Finding Optimal Plans for Domains with Continuous Effects with UPPAAL CORA. In Proceedings of the ICAPS'05 Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems, June 2005.
[ bib ]

[Die04]

H. Dierks. Heuristic guided model-checking of real-time systems. In P. Pettersson and Wang Yi, editors, Proceedings of the 16th Nordic Workshop on Programming Theory, number 2004-041 in Technical Reports of the Department of Information Technology, pages 14-16. Uppsala University, Sweden, October 2004.
[ bib ]

[DT03]

H. Dierks and J. Tapken. Moby/DC - A tool for model-checking parametric real-time specifications. In H. Garavel and J. Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), volume 2619 of LNCS, pages 271-277. Springer, 2003.
[ bib | .ps.gz ]

We define an operational subset of Duration Calculus, called phase automata, which serves as an intermediate language for the analysis and verification of real-time system descriptions that contain timing parameters. We introduce the tool Moby/DC which implements a model-checking algorithm for phase automata. The algorithm applies compositional model-checking techniques and handles parameters by built-in procedures or by a link to CLP(R). Due to the parameters the model-checking problem is undecidable in general. Hence, we have to accept that the results are overapproximations only in order to guarantee termination. The overapproximation together with the compositional technique makes the model-checker especially well suited for proving the absence of error traces instead of finding them.

[OD03]

E.-R. Olderog and H. Dierks. Moby/RT: A Tool for Specification and Verification of Real-Time Systems. Journal of Universal Computer Science, 9:88-105, 2003.
[ bib ]

The tool Moby/RT supports the design of real-time systems at the levels of requirements, design specifications and programs. Requirements are expressed by constraint diagrams [Kle00], design specifications by PLC-Automata [Die00], and programs by Structured Text, a programming language dedicated for programmable logic controllers (PLCs), or by programs for LEGO Mindstorm robots. In this paper we outline the theoretical background of Moby-RT by discussing its semantic basis and its use for automatic verification by utilising the model-checker UPPAAL.

References

[Kle00]

Kleuker, C. (2000). Constraint Diagrams. PhD thesis, University of Oldenburg.

[Die00]

Dierks, H. (2000). PLC-Automata: A New Class of Implementable Real-Time Automata. TCS, 253(1):61-93.

[DO03]

H. Dierks and E.-R. Olderog. Temporale Spezifikationslogiken. at-Automatisierungstechnik, 51(2):A1-A4, 2003.
[ bib ]

Logiken sind in der Informatik ein weitverbreitetes Mittel zur Spezifikation. Dazu werden Logiken verschiedener Ausprägung benutzt, z.B. temporale Logiken für reaktive Systeme, zu denen die Systeme der Automatisierungstechnik zählen. Dieser Beitrag enthält eine Einführung in die wichtigsten temporalen Logiken und Literaturverweise.

English
Logics are often used in computer science as specification languages. There is a rich variety of logics to choose from depending on the problem. Systems in automation technology are typically reactive systems for which temporal logics are adequate. We introduce the most important temporal logics and give reference for further reading.

[DBL02]

H. Dierks, G. Behrmann, and K.G. Larsen. Solving Planning Problems Using Real-Time Model-Checking (Translating PDDL3 into Timed Automata). In F. Kabanza and S. Thiebaux, editors, AIPS-Workshop Planning via Model-Checking, pages 30-39, April 2002.
[ bib | .ps.gz ]

[DL02]

H. Dierks and M. Lettrari. Constructing Test Automata from Graphical Real-Time Requirements. In FTRTFT 2002, Lecture Notes in Computer Science, pages 433-453. Springer-Verlag, September 2002.
[ bib | .ps.gz ]

[DT01]

H. Dierks and J. Tapken. Moby/PLC: Eine graphische Entwicklungsumgebung für SPS-Programme. at-Automatisierungstechnik, 1:38-44, 2001.
[ bib ]

[DT00]

H. Dierks and J. Tapken. Modelling and Verifying of `Cash-Point Service' Using Moby/PLC. Formal Aspects of Computing, 12:222-221, 2000.
[ bib | .ps.gz ]

[Die00b]

H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata . Theoret. Comput. Sci., 253(1):61-93, December 2000. full version of [Die97a].
[ bib ]

[Die00a]

H. Dierks. A Process Algebra for Real-Time Programs. In T. Maibaum, editor, FASE 2000: Fundamental Approaches to Software Engineering, volume 1783 of Lecture Notes in Computer Science, pages 66-81. Springer-Verlag, 2000.
[ bib ]

[Die00c]

H. Dierks. Specification and Verification of Polling Real-Time Systems. In H. Fiedler, O. Günther, W. Grass, S. Hölldobler, G. Hotz, R. Reischuk, B. Seeger, and D. Wagner, editors, Ausgezeichnete Informatikdissertationen 1999. Teubner, 2000.
[ bib | .ps.gz ]

[Die99]

H. Dierks. Synthesizing Controllers from Real-Time Specifications. IEEE Transactions on Computer-Aided Design of Integrated Circu its and Systems, 18(1):33-43, 1999.
[ bib | .ps.gz ]

[DFMV98a]

H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. In FTRTFT'98, Lecture Notes in Computer Science, pages 29-40. Springer-Verlag, 1998. (c) Springer-Verlag. This publication is available here and at Springer.
[ bib ]

[DFMV98b]

H. Dierks, A. Fehnker, A. Mader, and F.W. Vaandrager. Operational and Logical Semantics for Polling Real-Time Systems. Technical Report CSI-R9813, Computer Science Institue Nijmegen, Faculty of Mathematics and Informatics, Catholic University of Nijmegen, April 1998. full paper of [DFMV98a].
[ bib | .html ]

[Die98]

H. Dierks. Comparing Model-Checking and Logical Reasoning for Real-Time Systems. In ESSLLI'98, August 1998. Workshop proceedings.
[ bib | .ps.gz ]

[TD98]

J. Tapken and H. Dierks. Moby/PLC - Graphical Development of PLC-Automata. In A.P. Ravn and H. Rischel, editors, Proceedings of FTRTFT'98, volume 1486 of LNCS, pages 311-314. Springer Verlag, 1998. (c) Springer-Verlag. This publication is available here and at Springer.
[ bib ]

[DS98]

H. Dierks and M. Schenke. A Unifying Framework for Correct Program Construction. In J. Jeuring, editor, Mathematics of Program Construction 98, volume 1422 of Lecture Notes in Computer Science, pages 122-150. Springer-Verlag, June 1998. (c) Springer-Verlag. This publication is available here and at Springer.
[ bib ]

[DT98]

H. Dierks and J. Tapken. Tool-Supported Hierarchical Design of Distributed Real-Time Systems. In Euromicro Workshop on Real Time Systems, pages 222-229. IEEE, 1998.
[ bib | .ps.gz ]

[OD98]

E.-R. Olderog and H. Dierks. Decomposing Real-Time Specifications. In H. Langmaack, A. Pnueli, and W.P. de Roever, editors, Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science, pages 465-489. Springer-Verlag, 1998. An abstract is available on-line.
[ bib ]

[DD97]

Henning Dierks and Cheryl Dietz. Graphical Specification and Reasoning: Case Study Generalized Railroad Crossing. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, FME'97, volume 1313 of Lecture Notes in Computer Science, pages 20-39. Springer-Verlag, 1997.
[ bib | .ps.gz ]

[Die97b]

Henning Dierks. Synthesising Controllers from Real-Time Specifications. In Tenth International Symposium on System Synthesis, pages 126-133. IEEE CS Press, 1997.
[ bib | .ps.gz ]

[Die97a]

Henning Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata. In M. Bertran and T. Rus, editors, Transformation-Based Reactive Systems Development (ARTS'97), volume 1231 of Lecture Notes in Computer Science, pages 111-125. Springer-Verlag, 1997.
[ bib | .ps.gz ]

[Die96]

Henning Dierks. The production cell: A verified real-time system. In B. Jonsson and J. Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'96) (Uppsala, Sweden), volume 1135 of Lecture Notes in Computer Science, pages 208-227. Springer-Verlag, 1996.
[ bib | .ps.gz ]