Correct System Design

Dr. Josef Tapken

On this page:

back to the mainpage.

 

go next top of page

1 Publications (BibTeX Source)




@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{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},
}


@INPROCEEDINGS{jt99,
  AUTHOR = {Josef Tapken},
  TITLE = {{Implementing Hierarchical Graph-Structures}},
  BOOKTITLE = {Proceedings of FASE'99},
  EDITOR = {J.-P. Finance},
  VOLUME = {1577},
  SERIES = {LNCS},
  PUBLISHER = {Springer-Verlag},
  YEAR = {1999},
  PAGES = {219--233},
  NOTE = {\copyright Springer-Verlag. This publication is available
    {\url{http://csd.informatik.uni-oldenburg.de/pub/Papers/jt99.ps.gz}{here}}
    and at
    {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}}
}


@INPROCEEDINGS{jt98,
  AUTHOR = {J. Tapken},
  TITLE = {{Moby/PLC -- A Design Tool for Hierarchical Real-Time
Automata}},
  BOOKTITLE = {Proceedings of FASE'98},
  EDITOR = {E. Astesiano},
  VOLUME = {1382},
  SERIES = {LNCS},
  PUBLISHER = {Springer Verlag},
  YEAR = {1998},
  PAGES = {326-329},
}


@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{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{jt97-ess,
  AUTHOR = {Josef Tapken},
  TITLE = {{Interactive and Compilative Simulation of PLC-Automata}},
  BOOKTITLE = {Simulation in Industry, ESS'97},
  EDITOR = {Winfried Hahn and Axel Lehmann},
  PUBLISHER = {Society for Computer Simulation},
  YEAR = 1997,
  PAGES = {552--556},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/jt97-ess.ps.gz}
}


@INPROCEEDINGS{hfjt97,
  AUTHOR = {Hans Fleischhack and Josef Tapken},
  TITLE = {An {M-Net} Semantics for a Real-Time Extension of
{$\mu$SDL}},
  BOOKTITLE = {Formal Methods: Their Industrial Application and
    Strengthened Foundations (FME'97)},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1313,
  YEAR = 1997,
  PAGES = {162--181},
  URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hfjt97.ps.gz}
}


@INPROCEEDINGS{hfjt95,
  AUTHOR = {Hans Fleischhack and Josef Tapken},
  TITLE = {Eine kompositionelle {P}etrinetz-{S}emantik f\"ur
    {SDL}-{S}pezifikationen},
  BOOKTITLE = {2. Workshop Algorithmen und Werkzeuge f\"ur Petrinetze},
  EDITOR = {J. Desel and Hans Fleischhack and A. Oberweis and Michael
    Sonnenschein},
  NUMBER = {22},
  SERIES = {AIS reports},
  YEAR = 1995,
  ORGANIZATION = {Fachbereich Informatik},
  PUBLISHER = {Universit\"at Oldenburg}
}

 top of page go back