Dr. habil. Henning Dierks
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@INPROCEEDINGS{Die05b,
AUTHOR = {H. Dierks},
TITLE = {{Finding Optimal Plans for Domains with Continuous
Effects with UPPAAL CORA}},
BOOKTITLE = {{Proceedings of the ICAPS'05 Workshop on Verification
and Validation of Model-Based Planning and Scheduling Systems}},
MONTH = {June},
YEAR = {2005}
}
@INPROCEEDINGS{Die04b,
AUTHOR = {H. Dierks},
TITLE = {Heuristic Guided Model-Checking of Real-Time Systems},
EDITOR = {P. Pettersson and Wang Yi},
BOOKTITLE = {{Proceedings of the 16th Nordic Workshop on Programming Theory}},
PAGES = {14--16},
SERIES = {Technical Reports of the Department of Information Technology},
NUMBER = {2004-041},
PUBLISHER = {Uppsala University, Sweden},
ISSN = {1404-3203},
YEAR = {2004},
MONTH = {October}
}
@INPROCEEDINGS{DT03,
AUTHOR = {H. Dierks and J. Tapken},
TITLE = {{\sc Moby/DC} -- {A} Tool for Model-Checking
Parametric Real-Time Specifications},
BOOKTITLE = {Tools and Algorithms for the Construction and
Analysis of Systems (TACAS 2003)},
EDITOR = {H. Garavel and J. Hatcliff},
YEAR = {2003},
PAGES = {271--277},
SERIES = {LNCS},
VOLUME = 2619,
PUBLISHER = {Springer},
ABSTRACT = {
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.
},
URL = {http://csd.informatik.uni-oldenburg.de/~dierks/Berichte/TACAS03.ps.gz}
}
@ARTICLE{OD03,
AUTHOR = {E.-R. Olderog and H. Dierks},
TITLE = {{Moby/RT: A Tool for Specification and Verification of
Real-Time Systems}},
JOURNAL = {Journal of Universal Computer Science},
YEAR = {2003},
VOLUME = {9},
PAGES = {88--105},
ABSTRACT = {
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.
\begin{thebibliography}
\bibitem{Kle00}
Kleuker, C. (2000).
\newblock {\em {Constraint Diagrams}}.
\newblock PhD thesis, University of Oldenburg.
\bibitem[Dierks, 2000]{Die00}
Dierks, H. (2000).
\newblock {PLC-Automata: A New Class of Implementable Real-Time Automata}.
\newblock {\em TCS}, 253(1):61--93.
\end{thebibliography}
}
}
@ARTICLE{DO03,
AUTHOR = {H. Dierks and E.-R. Olderog},
TITLE = {{Temporale Spezifikationslogiken}},
JOURNAL = {at-Automatisierungstechnik},
YEAR = {2003},
VOLUME = {51},
NUMBER = {2},
PAGES = {A1--A4},
ABSTRACT = {
Logiken sind in der Informatik ein weitverbreitetes Mittel zur
Spezifikation. Dazu werden Logiken verschiedener Auspr{\"a}gung
benutzt, z.B. temporale Logiken f{\"u}r reaktive Systeme, zu
denen die Systeme der Automatisierungstechnik z{\"a}hlen. Dieser
Beitrag enth{\"a}lt eine Einf{\"u}hrung in die wichtigsten
temporalen Logiken und Literaturverweise.
\textbf{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.
}
}
@INPROCEEDINGS{DBL02,
AUTHOR = {H. Dierks and G. Behrmann and K.G. Larsen},
TITLE = {{Solving Planning Problems Using Real-Time Model-Checking
(Translating PDDL3 into Timed Automata)}},
BOOKTITLE = {{AIPS-Workshop Planning via Model-Checking}},
PAGES = {30--39},
YEAR = {2002},
EDITOR = {F. Kabanza and S. Thiebaux},
MONTH = APR,
URL = {http://csd.Informatik.Uni-Oldenburg.DE/~dierks/Berichte/AIPS.ps.gz}
}
@INPROCEEDINGS{DL02,
AUTHOR = {H. Dierks and M. Lettrari},
TITLE = {{Constructing Test Automata from Graphical Real-Time
Requirements}},
BOOKTITLE = {FTRTFT 2002},
PAGES = {433--453},
YEAR = {2002},
SERIES = {Lecture Notes in Computer Science},
MONTH = SEP,
PUBLISHER = {Springer-Verlag},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/~dierks/Berichte/FTRTFT02.ps.gz}
}
@ARTICLE{dt01,
AUTHOR = {H. Dierks and J. Tapken},
TITLE = {{Moby/PLC: Eine graphische Entwicklungsumgebung f{\"u}r
SPS-Programme}},
JOURNAL = {at-Automatisierungstechnik},
YEAR = {2001},
VOLUME = {1},
PAGES = {38--44},
}
@ARTICLE{dt00,
AUTHOR = {H. Dierks and J. Tapken},
TITLE = {{Modelling and Verifying of `Cash-Point Service' Using
Moby/PLC}},
JOURNAL = {Formal Aspects of Computing},
YEAR = {2000},
VOLUME = {12},
PAGES = {222--221},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hdjt00.ps.gz},
}
@ARTICLE{die00,
AUTHOR = {H. Dierks},
TITLE = {{PLC-Automata: A New Class of Implementable Real-Time
Automata }},
JOURNAL = {Theoret.\ Comput.\ Sci.},
YEAR = {2000},
VOLUME = {253},
NUMBER = {1},
MONTH = DEC,
PAGES = {61--93},
NOTE = {full version of \cite{hd97-arts}},
}
@INPROCEEDINGS{die00b,
AUTHOR = {H. Dierks},
TITLE = {{A Process Algebra for Real-Time Programs}},
BOOKTITLE = {FASE 2000: Fundamental Approaches to Software
Engineering},
EDITOR = {T. Maibaum},
VOLUME = {1783},
SERIES = {Lecture Notes in Computer Science},
YEAR = {2000},
PUBLISHER = {Springer-Verlag},
PAGES = {66--81},
}
@INPROCEEDINGS{die00c,
AUTHOR = {H. Dierks},
TITLE = {{Specification and Verification of Polling Real-Time
Systems}},
BOOKTITLE = {{Ausgezeichnete Informatikdissertationen 1999}},
EDITOR = {H. Fiedler and O. G{\"u}nther and W. Grass and
S. H{\"o}lldobler and G. Hotz and R. Reischuk and B. Seeger and D. Wagner},
YEAR = {2000},
PUBLISHER = {Teubner},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hd00.ps.gz},
}
@ARTICLE{die99,
AUTHOR = {H. Dierks},
TITLE = {{Synthesizing Controllers from Real-Time Specifications}},
JOURNAL = {IEEE Transactions on Computer-Aided Design of Integrated
Circu its and Systems},
YEAR = {1999},
VOLUME = {18},
NUMBER = {1},
PAGES = {33--43},
URL = {http://csd.Informatik.Uni-Oldenburg.DE/~dierks/Berichte/TCAD.ps.gz}
}
@INPROCEEDINGS{hd98c,
AUTHOR = {H. Dierks and A. Fehnker and A. Mader and F.W. Vaandrager},
TITLE = {{Operational and Logical Semantics for Polling Real-Time
Systems}},
BOOKTITLE = {FTRTFT'98},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1998},
PUBLISHER = {Springer-Verlag},
PAGES = {29--40},
NOTE = {\copyright Springer-Verlag. This publication is available
{\url{http://csd.Informatik.Uni-Oldenburg.DE/~dierks/Berichte/FTRTFT98.ps.gz}{
here}}
and at
{\url{http://www.springer.de/comp/lncs/index.html}{Springer}}}
}
@TECHREPORT{hd98b,
AUTHOR = {H. Dierks and A. Fehnker and A. Mader and F.W. Vaandrager},
TITLE = {{Operational and Logical Semantics for Polling Real-Time
Systems}},
INSTITUTION = {Computer Science Institue Nijmegen, Faculty of Mathematics
and Informatics, Catholic University of Nijmegen},
YEAR = {1998},
NUMBER = {CSI-R9813},
MONTH = APR,
NOTE = {full paper of \cite{hd98c}.},
URL = {http://www.cs.kun.nl/csi/reports/info/CSI-R9813.html}
}
@INPROCEEDINGS{hd98a,
AUTHOR = {H. Dierks},
TITLE = {{Comparing Model-Checking and Logical Reasoning for
Real-Time Systems}},
BOOKTITLE = {ESSLLI'98},
YEAR = {1998},
MONTH = AUG,
NOTE = {Workshop proceedings},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ESSLLI.ps.gz}
}
@INPROCEEDINGS{jthd98,
AUTHOR = {J. Tapken and H. Dierks},
TITLE = {{Moby/PLC -- Graphical Development of PLC-Automata}},
BOOKTITLE = {Proceedings of FTRTFT'98},
EDITOR = {A.P. Ravn and H. Rischel},
VOLUME = {1486},
SERIES = {LNCS},
PUBLISHER = {Springer Verlag},
YEAR = {1998},
PAGES = {311-314},
NOTE = {\copyright Springer-Verlag. This publication is available
{\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/jthd98.ps.gz}{here}}
and at
{\url{http://www.springer.de/comp/lncs/index.html}{Springer}}},
}
@INPROCEEDINGS{hdms98,
AUTHOR = {H. Dierks and M. Schenke},
TITLE = {{A Unifying Framework for Correct Program Construction}},
BOOKTITLE = {Mathematics of Program Construction 98},
EDITOR = {J. Jeuring},
VOLUME = {1422},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1998},
PUBLISHER = {Springer-Verlag},
MONTH = JUN,
PAGES = {122--150},
NOTE = {\copyright Springer-Verlag. This publication is available
{\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/MPC.ps.gz}{here}}
and at
{\url{http://www.springer.de/comp/lncs/index.html}{Springer}}}
}
@INPROCEEDINGS{hdjt98,
AUTHOR = {H. Dierks and J. Tapken},
TITLE = {{Tool-Supported Hierarchical Design of Distributed
Real-Time Systems}},
BOOKTITLE = {Euromicro Workshop on Real Time Systems},
PUBLISHER = {IEEE},
YEAR = {1998},
PAGES = {222-229},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hdjt98.ps.gz}
}
@INPROCEEDINGS{erohd98,
AUTHOR = {E.-R. Olderog and H. Dierks},
TITLE = {{Decomposing Real-Time Specifications}},
BOOKTITLE = {{Compositionality: The Significant Difference}},
EDITOR = {H. Langmaack and A. Pnueli and W.P. de Roever},
VOLUME = {1536},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1998},
PUBLISHER = {Springer-Verlag},
PAGES = {465--489},
NOTE = {{\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/erohd97.ps.gz}
{An abstract is available on-line}}}
}
@INPROCEEDINGS{hdcd97,
AUTHOR = {Henning Dierks and Cheryl Dietz},
TITLE = {{Graphical Specification and Reasoning: Case Study
"Generalized Railroad Crossing"}},
BOOKTITLE = {FME'97},
EDITOR = {J. Fitzgerald and C.B. Jones and P. Lucas},
VOLUME = 1313,
SERIES = {Lecture Notes in Computer Science},
YEAR = 1997,
PUBLISHER = {Springer-Verlag},
PAGES = {20--39},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hdcd97-fme.ps.gz}
}
@INPROCEEDINGS{hd97-isss,
AUTHOR = {Henning Dierks},
TITLE = {{Synthesising Controllers from Real-Time Specifications}},
BOOKTITLE = {{Tenth International Symposium on System Synthesis}},
YEAR = {1997},
PUBLISHER = {IEEE CS Press},
OPTMONTH = SEP,
PAGES = {126--133},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hd97-isss.ps.gz}
}
@INPROCEEDINGS{hd97-arts,
AUTHOR = {Henning Dierks},
TITLE = {{PLC-Automata: A New Class of Implementable Real-Time
Automata}},
BOOKTITLE = {Transformation-Based Reactive Systems Development
(ARTS'97)},
EDITOR = {M. Bertran and T. Rus},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1231},
YEAR = {1997},
PUBLISHER = {Springer-Verlag},
PAGES = {111--125},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hd97-arts.ps.gz}
}
@INPROCEEDINGS{hd96,
AUTHOR = {Henning Dierks},
TITLE = {The Production Cell: A Verified Real-Time System},
BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems
(FTRTFT'96) (Uppsala, Sweden)},
EDITOR = {B. Jonsson and J. Parrow},
VOLUME = {1135},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
YEAR = 1996,
PAGES = {208--227},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/FTRTFT96.ps.gz}
}
