Publications
Contact
 Head
Prof. Dr. ErnstRüdiger Olderog  Secretary
Andrea Göken
Tel.: +49(0)4417983121
Fax.: +49(0)4417982965
Mail: Andrea.Goeken@informlyfatik.uniold_{dc4+b}enxjbumfkp2rgch.dlndefh
Room: A3 2208
Latest Publications

[article] bibtex  Go to documentM. Schwammberger, "An Abstract Model for Proving Safety of Autonomous Urban Traffic," Theoretical Computer Science, vol. 744, pp. 143169, 2018.
@article{Schwammberger18b, title = {An Abstract Model for Proving Safety of Autonomous Urban Traffic},
author = {M. Schwammberger},
journal = {Theoretical Computer Science},
volume = {744},
year = {2018},
pages = {143169},
url = {https://doi.org/10.1016/j.tcs.2018.05.028} } 
[inproceedings] bibtex  Go to documentM. Schwammberger, "Introducing Liveness into Multilane Spatial Logic lane change controllers using UPPAAL," in Proc. Proceedings 2nd International Workshop on Safe Control of Autonomous Vehicles, SCAV@CPSWeek 2018, Porto, Portugal, 10th April 2018., 2018, pp. 1731.
@inproceedings{Schwammberger18a,
author = {Maike Schwammberger},
title = {Introducing Liveness into Multilane Spatial Logic lane change controllers using {UPPAAL}},
editor = {Mario Gleirscher and Stefan Kugele and Sven Linker},
booktitle = {Proceedings 2nd International Workshop on Safe Control of Autonomous Vehicles, SCAV@CPSWeek 2018, Porto, Portugal, 10th April 2018.},
series = {{EPTCS}},
volume = {269},
pages = {1731},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.269.3} } 
[inproceedings] bibtex  Go to documentE. R. Olderog, "Space for Traffic Manoeuvres  An Overview," in Proc. Symposium on RealTime and Hybrid Systems, 2018, pp. 211230.
@inproceedings{Olderog18,
author = {E.R. Olderog},
title = {Space for Traffic Manoeuvres  An Overview},
editor = {Cliff Jones and Ji Wang and Naijun Zhan},
booktitle = {Symposium on RealTime and Hybrid Systems},
pages = {211230},
series = {LNCS},
volume = {11180},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/9783030014612_11} } 
[article] bibtex  Go to documentM. Schwammberger, "An abstract model for proving safety of autonomous urban traffic," Theor. Comput. Sci., vol. 744, pp. 143169, 2018.
@article{DBLP:journals/tcs/Schwammberger18,
author = {Maike Schwammberger},
title = {An abstract model for proving safety of autonomous urban traffic},
journal = {Theor. Comput. Sci.},
volume = {744},
pages = {143169},
year = {2018},
url = {https://doi.org/10.1016/j.tcs.2018.05.028},
doi = {10.1016/j.tcs.2018.05.028},
timestamp = {Fri, 28 Sep 2018 17:00:52 +0200},
biburl = {https://dblp.org/rec/bib/journals/tcs/Schwammberger18},
bibsource = {dblp computer science bibliography, https://dblp.org} } 
[book] bibtex  Go to documentProvably Correct Systems, Hinchey, M. G., Bowen, J. P., and Olderog, E. R., Eds., SpringerVerlag, 2017.
@book{HBO17, editor = {M. G. Hinchey and J. P. Bowen and E.R. Olderog },
title = {Provably Correct Systems},
series = {NASA Monographs in System and Software Engineering},
publisher = {SpringerVerlag},
year = {2017},
note = {328 pp, ISBN 9783319486277},
url = {https://link.springer.com/book/10.1007/9783319486284} } 
[article] bibtex  Go to documentB. Finkbeiner and E. R. Olderog, "Petri Games: Synthesis of Distributed Systems with Causal Memory," Information and Computation, vol. 253, Part 2, pp. 181203, 2017.
@article{FinkbeinerOlderog16, title = {Petri Games: Synthesis of Distributed Systems with Causal Memory},
author = {B. Finkbeiner and E.R. Olderog},
journal = {Information and Computation},
volume = {253, Part 2 },
year = {2017},
pages = {181203},
url = {https://www.unioldenburg.de/fileadmin/user_upload/f2informcsd/pub/mainPGIC.pdf},
abstract = {We present a new multiplayer game model for the interaction and the flow of information in a distributed system. The players are tokens on a Petri net. As long as the players move in independent parts of the net, they do not know of each other; when they synchronize at a joint transition, each player gets informed of the causal history of the other player. We show that for Petri games with a single environment player and an arbitrary bounded number of system players, deciding the existence of a safety strategy for the system players is EXPTIMEcomplete.} } 
[article] bibtex  Go to documentG. v. Bochmann, M. Hilscher, S. Linker, and E. R. Olderog, "Synthesizing and Verifying Controllers for Multilane Traffic Maneuvers," Formal Aspects of Computing, vol. 29, iss. 4, pp. 583600, 2017.
@article{BHLO17,
author = {G. v. Bochmann and M. Hilscher and S. Linker and E.R. Olderog},
title = {Synthesizing and Verifying Controllers for Multilane Traffic Maneuvers},
journal = {Formal Aspects of Computing},
volume = {29},
number = {4},
year = {2017},
pages = {583600},
doi = {10.1007/s0016501704244},
url = {https://www.unioldenburg.de/fileadmin/user_upload/informatik/ag/csd/pub/faocsynthesis.pdf} } 
[incollection] bibtex  Go to documentE. R. Olderog, A.P.Ravn, and R. Wisniewski, "Linking Discrete and Dynamic Models: Applied to Traffic Manoevres," in Provably Correct Systems, Hinchey, M. G., Bowen, J. P., and Olderog, E. R., Eds., Springer, 2017, pp. 95120.
@incollection{ORW17,
author = {E.R. Olderog and A.P.Ravn and R. Wisniewski},
title = {Linking Discrete and Dynamic Models: Applied to Traffic Manoevres},
editor = {M.G. Hinchey and J.P. Bowen and E.R. Olderog},
booktitle = {Provably Correct Systems},
note = {NASA Monographs in Systems and Software Engineering},
publisher = {Springer},
year = {2017},
pages = {95120},
url = {https://www.unioldenburg.de/fileadmin/user_upload/informatik/ag/csd/pub/mainORW.pdf} } 
[inproceedings] bibtex  Go to documentM. Schwammberger, "Imperfect Knowledge in Autonomous Urban Traffic Manoeuvres," in Proc. Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@iFM 2017, Turin, Italy, 19th September 2017., 2017, pp. 5974.
@inproceedings{DBLP:journals/corr/abs170902559,
author = {Maike Schwammberger},
title = {Imperfect Knowledge in Autonomous Urban Traffic Manoeuvres},
booktitle = {Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@iFM 2017, Turin, Italy, 19th September 2017.},
pages = {5974},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.257.7},
doi = {10.4204/EPTCS.257.7},
timestamp = {Mon, 16 Oct 2017 16:32:11 +0200},
biburl = {http://dblp.org/rec/bib/journals/corr/abs170902559},
bibsource = {dblp computer science bibliography, http://dblp.org} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and M. Schwammberger, "Formalising a Hazard Warning Communication Protocol with Timed Automata," in Proc. Models, Algorithms, Logics and Tools, 2017, pp. 640660.
@inproceedings{OlderogSchwammberger17,
author = {E.R. Olderog and M. Schwammberger},
title = {Formalising a Hazard Warning Communication Protocol with Timed Automata},
editor = {Luca Aceto and Giorgio Bacci and Giovanni Bacci and Anna Ing{\'{o}}lfsd{\'{o}}ttir and Axel Legay and Radu Mardare},
booktitle = {Models, Algorithms, Logics and Tools},
pages = {640660},
series = {LNCS},
volume = {10460},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/9783319631219_32} } 
[inproceedings] bibtex  Go to documentB. Finkbeiner, M. Gieseking, J. HeckingHarbusch, and E. Olderog, "Symbolic vs. Bounded Synthesis for Petri Games," in Proc. Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017, 2017, pp. 2343.
@inproceedings{DBLP:journals/corr/abs171110637,
author = {Finkbeiner, Bernd and Gieseking, Manuel and HeckingHarbusch, Jesko and Olderog, ErnstR\"udiger},
year = {2017},
title = {Symbolic vs. Bounded Synthesis for Petri Games},
editor = {Fisman, Dana and Jacobs, Swen},
booktitle = {Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017},
series = {Electronic Proceedings in Theoretical Computer Science {(EPTCS)}},
volume = {260},
publisher = {Open Publishing Association},
pages = {2343},
doi = {10.4204/EPTCS.260.5},
url = {https://arxiv.org/abs/1711.10637} } 
[inproceedings] bibtex  Go to documentH. Ody, "Monitoring of Traffic Manoeuvres with Imprecise Information," in Proc. Proceedings First Workshop on Formal Verification of Autonomous Vehicles, Turin, Italy, 19th September 2017, 2017, pp. 4358.
@inproceedings{Ody17,
author = {Ody, Heinrich},
year = {2017},
title = {Monitoring of Traffic Manoeuvres with Imprecise Information},
editor = {Bulwahn, Lukas and Kamali, Maryam and Linker, Sven},
booktitle = {{Proceedings First Workshop on} Formal Verification of Autonomous Vehicles, {Turin, Italy, 19th September 2017}},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {257},
publisher = {Open Publishing Association},
pages = {4358},
doi = {10.4204/EPTCS.257.6},
url = {https://arxiv.org/abs/1709.02558v1} } 
[inproceedings] bibtex  Go to documentB. Engelmann and E. Olderog, "A Sound and Complete Hoare Logic for DynamicallyTyped, ObjectOriented Programs," in Proc. Proc. Theory and Practice of Formal Methods, 2016, pp. 173193.
@inproceedings{EngelmannOlderog2015,
author = {Bj\"orn Engelmann and ErnstR\"udiger Olderog},
title = {{A} {S}ound and {C}omplete {H}oare {L}ogic for {D}ynamically{T}yped, {O}bject{O}riented {P}rograms},
booktitle = {Proc. Theory and Practice of Formal Methods},
year = {2016},
editor = {Erika {\' A}brah{\' a}m and Marcello Bonsangue and Einar Broch Johnsen},
volume = {9660},
series = {LNCS},
publisher = {Springer},
pages = {173193},
url = {http://link.springer.com/chapter/10.1007%2F9783319307343_13},
optaddress = {Eindhoven, The Netherlands} } 
[inproceedings] bibtexM. Hilscher and M. Schwammberger, "An Abstract Model for Proving Safety of Autonomous Urban Traffic," in Proc. Theoretical Aspects of Computing (ICTAC), 2016, pp. 274292.
@inproceedings{HS16,
author = {Hilscher, Martin and Schwammberger, Maike},
editor = {Sampaio, Augusto and Wang, Farn},
title = {An Abstract Model for Proving Safety of Autonomous Urban Traffic},
booktitle = {Theoretical Aspects of Computing (ICTAC)},
optbooktitle = {Theoretical Aspects of Computing  ICTAC 2016: 13th International Colloquium, Taipei, Taiwan, ROC, October 2431, 2016, Proceedings},
year = {2016},
publisher = {Springer},
optaddress = {Cham},
volume = {9965},
series = {LNCS},
pages = {274292},
isbn = {9783319467504},
doi = {10.1007/9783319467504_16} } 
[inproceedings] bibtex  Go to documentH. Ody, M. Fränzle, and M. R. Hansen, "Discounted Duration Calculus," in Proc. FM 2016: Formal Methods  21st International Symposium, Limassol, Cyprus, November 911, 2016, Proceedings, 2016, pp. 577592.
@inproceedings{OFH16,
author = {Heinrich Ody and Martin Fr{\"{a}}nzle and Michael R. Hansen},
editor = {John S. Fitzgerald and Constance L. Heitmeyer and Stefania Gnesi and Anna Philippou},
title = {Discounted Duration Calculus},
booktitle = {{FM} 2016: Formal Methods  21st International Symposium, Limassol, Cyprus, November 911, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9995},
pages = {577592},
year = {2016},
url = {http://theoretica.informatik.unioldenburg.de/~sefie/files/discounteddurationcalculus.pdf},
doi = {10.1007/9783319489896_35},
timestamp = {Mon, 22 May 2017 17:11:19 +0200},
biburl = {http://dblp.unitrier.de/rec/bib/conf/fm/OdyFH16},
bibsource = {dblp computer science bibliography, http://dblp.org} } 
[inproceedings] bibtex  Go to documentB. Engelmann, "Formally Verifying Dynamicallytyped Programs like Staticallytyped Ones  Another perspective," in Proc. Proceedings of the Young Researchers Conference Frontiers of Formal Methods, 2015.
@inproceedings{Eng2015,
author = {Bj{\"o}rn Engelmann},
title = {Formally Verifying Dynamicallytyped Programs like Staticallytyped Ones  Another perspective},
booktitle = {Proceedings of the Young Researchers Conference Frontiers of Formal Methods},
year = {2015},
url = {http://sunsite.informatik.rwthaachen.de/Publications/AIB/2015/201506.pdf} } 
[inproceedings] bibtexM. Schwammberger, "Properties of Communicating Controllers for Safe Traffic Manoeuvres," in Proc. Proceedings of the Doctoral Symposium of Formal Methods 2015, 2015, pp. 37.
@inproceedings{MS15,
author = {Maike Schwammberger},
title = {Properties of Communicating Controllers for Safe Traffic Manoeuvres},
booktitle = {Proceedings of the Doctoral Symposium of Formal Methods 2015},
editor = {Aichernig, Bernhard K. and Rossini, Alessandro},
pages = {37},
year = 2015 } 
[article] bibtex  Go to documentE. R. Olderog and M. Swaminathan, "Structural Transformations for DataEnriched RealTime Systems," Formal Asp. Comput., vol. 27, pp. 727750, 2015.
@article{OlderogSwaminathan14,
author = {E.R Olderog and M. Swaminathan},
title = {Structural Transformations for DataEnriched RealTime Systems},
journal = {Formal Asp. Comput.},
volume = {27},
pages = {727750},
year = {2015},
url = {http://dx.doi.org/10.1007/s001650140306y} } 
[misc] bibtex  Go to documentB. Engelmann, E. R. Olderog, and N. Flick, Closing the Gap  Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic, 2015.
@misc{EOF2015,
author = {Bj{\"o}rn Engelmann and E.R Olderog and NilsErik Flick},
title = {Closing the Gap  Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic},
month = {January},
year = {2015},
howpublished = {arXiv:1501.02699v1 [cs.PL]},
abstract = {Dynamically typed objectoriented languages enable programmers to write elegant, reusable and extensible programs. However, with the current methodology for program verification, the absence of static type information creates significant overhead. Our proposal is twofold: First, we propose a layer of abstraction hiding the complexity of dynamic typing when provided with sufficient type information. Since this essentially creates the illusion of verifying a staticallytyped program, the effort required is equivalent to the staticallytyped case. Second, we show how the required type information can be efficiently derived for all typesafe programs by integrating a type inference algorithm into Hoare logic, yielding a semiautomatic procedure allowing the user to focus on those typing problems really requiring his attention. While applying type inference to dynamically typed programs is a wellestablished method by now, our approach complements conventional soft typing systems by offering formal proof as a third option besides modifying the program (static typing) and accepting the presence of runtime type errors (dynamic typing).},
url = {http://arxiv.org/abs/1501.02699} } 
[techreport] bibtex  Go to documentM. Fränzle, M. R. Hansen, and H. Ody, "Discounted Duration Calculus," School of Computer Science, Reykjavik University, RUTRSCS16001, 2015.
@techreport{FHO15b, title = {Discounted Duration Calculus},
author = {Fr{\"a}nzle, Martin and Hansen, Michael R. and Ody, Heinrich},
year = {2015},
booktitle = {Nordic Workshop on Programming Theory  NWPT},
editor = {Luca Aceto, Ignacio Fabregas, Alvaro GarciaPerez and Anna Ingolfsdottir},
institution = {School of Computer Science, Reykjavik University},
number = {RUTRSCS16001},
url = {http://icetcs.ru.is/nwpt2015/NWPT15Proceedings.pdf} } 
[article] bibtex  Go to documentS. Linker and M. Hilscher, "Proof Theory of a MultiLane Spatial Logic," Logical Methods in Computer Science, vol. 11, iss. 3, 2015.
@article{LH15,
author = {S. Linker and M. Hilscher},
editor = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
title = {Proof Theory of a MultiLane Spatial Logic},
journal = {Logical Methods in Computer Science},
volume = {11},
number = {3},
pages = {},
year = {2015},
url = {http://www.lmcsonline.org/ojs/regularIssues.php?id=46} } 
[inproceedings] bibtex  Go to documentM. Gieseking, "Trace Refinement of $\pi$Calculus Processes," in Proc. Frontiers of Formal Methods 2015, 2015, pp. 109114.
@inproceedings{gie2015, booktitle = {Frontiers of Formal Methods 2015},
type = {Technical Report},
organization = {RWTH Aachen},
month = {February},
title = {Trace Refinement of $\pi$Calculus Processes},
author = {Manuel Gieseking},
year = {2015},
series = {Proceedings of the Young Researchers' Conference "Frontiers of Formal Methods"},
pages = {109114},
url = {http://www.unioldenburg.de/fileadmin/user\_upload/f2informcsd/gieseking15\_ffm.pdf} } 
[inproceedings] bibtex  Go to documentM. Fränzle, M. R. Hansen, and H. Ody, "No Need Knowing Numerous Neighbours  Towards a Realizable Interpretation of MLSL," in Proc. Correct System Design, 2015, pp. 152171.
@inproceedings{FHO15a,
author = {Martin Fr{\"{a}}nzle and Michael R. Hansen and Heinrich Ody},
title = {No Need Knowing Numerous Neighbours  Towards a Realizable Interpretation of {MLSL}},
editor = {Roland Meyer and Andr{\'{e}} Platzer and Heike Wehrheim},
booktitle = {Correct System Design},
pages = {152171},
year = {2015},
series = {Lecture Notes in Computer Science},
volume = {9360},
publisher = {Springer},
url = {http://theoretica.informatik.unioldenburg.de/~sefie/files/neighbourscsd15.pdf},
doi = {10.1007/9783319235066_11},
biburl = {http://dblp.unitrier.de/rec/bib/conf/birthday/FranzleHO15},
bibsource = {dblp computer science bibliography, http://dblp.org} } 
[inproceedings] bibtex  Go to documentE. R. Olderog, A. P. Ravn, and R. Wisniewski, "Linking Spatial and Dynamic Models for Traffic Maneuvers," in Proc. 54th IEEE Conf. on Decision and Control (CDC), Osaka, Japan, 2015, pp. 68096816.
@inproceedings{ORW2015,
author = {E.R. Olderog and A.P. Ravn and R. Wisniewski},
title = {Linking Spatial and Dynamic Models for Traffic Maneuvers},
booktitle = {54th IEEE Conf. on Decision and Control (CDC), Osaka, Japan },
year = {2015},
pages = {68096816},
month = {Dec},
publisher = {IEEE},
url = {https://www.unioldenburg.de/fileadmin/user_upload/f2informcsd/pub/rootORW15.pdf},
doi = {10.1109/CDC.2015.7403292},
subproject = {H3},
conferenceshort = {CDC},
conferencelong = {IEEE Conference on Decision and Control},
abstract = {For traffic maneuvers of multiple vehicles on highways we build an abstract spatial and a concrete dynamic model. In the spatial model we show the safety (collision freedom) of lanechange maneuvers. By linking the spatial and dynamic model via suitable refinements of the spatial atoms to distance measures, the safety carries over to the concrete mode} } 
[inproceedings] bibtex  Go to documentH. Ody, "Undecidability Results for MultiLane Spatial Logic," in Proc. Theoretical Aspects of Computing  ICTAC, 2015, pp. 404421.
@inproceedings{Ody15b,
author = {Heinrich Ody},
title = {Undecidability Results for MultiLane Spatial Logic},
booktitle = {Theoretical Aspects of Computing  {ICTAC}},
pages = {404421},
year = {2015},
editor = {Martin Leucker and Camilo Rueda and Frank D. Valencia},
volume = {9399},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
url = {http://theoretica.informatik.unioldenburg.de/~sefie/files/mlslundecictac15.pdf},
doi = {10.1007/9783319251509_24},
biburl = {http://dblp.unitrier.de/rec/bib/conf/ictac/Ody15},
bibsource = {dblp computer science bibliography, http://dblp.org} } 
[inproceedings] bibtexG. v. Bochmann, M. Hilscher, S. Linker, and E. Olderog, "Synthesizing Controllers for MultiLane Traffic Maneuvers," in Proc. International Symposium on Dependable Software Engineering (SETTA), 2015, pp. 7186.
@inproceedings{avacsh3dec15, title = {Synthesizing Controllers for MultiLane Traffic Maneuvers},
author = {Gregor v. Bochmann AND Martin Hilscher AND Sven Linker AND ErnstRüdiger Olderog},
editor = {Xuandong Li AND Zhiming Liu AND Wang Yi},
booktitle = {International Symposium on Dependable Software Engineering (SETTA)},
year = {2015},
month = {Nov.},
pages = {7186},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 9409, abstract = {The dynamic behavior of a car can be modeled as a hybrid system involving continuous state changes and discrete state transitions. However, we show that the control of safe (collision free) lane change maneuvers in multilane traffic on highways can be described by finite state machines extended with continuousvariables coming from the environment. We use standard theory for controller synthesis to derive the dynamic behavior of a lanechange controller. Thereby, we contrast the setting of interleaving semantics and synchronous concurrent semantics. We also consider the possibility of exchanging knowledge between neighboring cars in order to come up with the right decisions.},
conferencelong = {International Symposium on Dependable Software Engineering},
conferenceshort = {SETTA} } 
[inproceedings] bibtex  Go to documentB. Finkbeiner, M. Gieseking, and E. Olderog, "Adam: CausalityBased Synthesis of Distributed Systems," in Proc. Computer Aided Verification  27th International Conference, CAV 2015, San Francisco, CA, USA, July 1824, 2015, Proceedings, Part I, 2015, pp. 433439.
@inproceedings{fingieold15, title = {Adam: CausalityBased Synthesis of Distributed Systems},
author = {Bernd Finkbeiner and Manuel Gieseking and ErnstR{\"{u}}diger Olderog},
booktitle = {Computer Aided Verification  27th International Conference, {CAV} 2015, San Francisco, CA, USA, July 1824, 2015, Proceedings, Part {I}},
year = {2015},
editor = {Daniel Kroening and Corina S. Pasareanu},
pages = {433439},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {9206},
abstract = {We present ADAM, a tool for the automatic synthesis of distributed systems with multiple concurrent processes. For each process, an individual controller is synthesized that acts on locally available information obtained through synchronization with the environment and with other system processes. ADAM is based on Petri games, an extension of Petri nets where each token is a player in a multiplayer game. ADAM implements the first symbolic game solving algorithm for Petri games. We report on experience from several case studies with up to 38 system processes.},
conferencelong = {International Conference on Computer Aided Verification},
conferenceshort = {CAV},
url = {http://www.unioldenburg.de/fileadmin/user\_upload/f2informcsd/fingieold15.pdf} } 
[techreport] bibtex  Go to documentH. Ody, "Undecidability Results for MultiLane Spatial Logic," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 112, 2015.
@techreport{Ody15a, title = {Undecidability Results for MultiLane Spatial Logic},
author = {Heinrich Ody},
institution = {SFB/TR 14 AVACS},
year = {2015},
month = {September},
note = {http://www.avacs.org},
number = {112},
type = {Reports of SFB/TR 14 AVACS},
abstract = {We consider (un)decidability of MultiLane Spatial Logic (MLSL), a multidimensional modal logic introduced for reasoning about traffic manoeuvres. MLSL with length measurement has been shown to be undecidable. However, the proof relies on exact values. This raises the question whether the logic remains undecidable when we consider robust satisfiability, i.e. when values are known only approximately. Our main result is that robust satisfiability of MLSL is undecidable. Furthermore, we prove that even MLSL without length measurement is undecidable. In both cases we reduce the intersection emptiness of two contextfree languages to the respective satisfiability problem. This is the full version of a paper with the same title published at the ICTAC 2015.},
access = {open},
bibtex = {atr112.bib},
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
pdf = {avacs_technical_report_112.pdf},
url = {http://www.avacs.org/fileadmin/Publikationen/Open/avacs\_technical\_report\_112.pdf},
series = {ATR},
subproject = {H3,R1} } 
[inproceedings] bibtex  Go to documentN. Flick and B. Engelmann, "Properties of Petri Nets with Contextfree Structure Changes," in Proc. Fifth International Workshop on Graph Computation Models, 2014.
@inproceedings{FE2014,
author = {NilsErik Flick and Bj{\"o}rn Engelmann},
title = {Properties of Petri Nets with Contextfree Structure Changes},
booktitle = {Fifth International Workshop on Graph Computation Models},
year = {2014},
abstract = {Petri nets model systems with distributed state and syn chronised state changes. Extending them with rewriting rules allows for evolving structure. In this paper, we investigate dynamic properties of simple structurechanging Petri nets. We show undecidability of checking a languagebased notion of correctness even for very restricted classes of structurechanging nets. We also introduce a colourbased abstraction and use it to specify, and in special cases decide, reachability properties.},
url = {http://gcm2014.imag.fr/proceedingsGCM2014.pdf} } 
[inproceedings] bibtex  Go to documentB. Finkbeiner and E. R. Olderog, "Petri Games: Synthesis of Distributed Systems with Causal Memory," in Proc. Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 1012, 2014., 2014, pp. 217230.
@inproceedings{FinOld14,
author = {Bernd Finkbeiner and E.R Olderog},
title = {Petri Games: Synthesis of Distributed Systems with Causal Memory},
editor = {Adriano Peron and Carla Piazza},
booktitle = {Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014, Verona, Italy, September 1012, 2014.},
series = {{EPTCS}},
year = {2014},
volume = {161},
pages = {217230},
url = {http://arxiv.org/abs/1406.1069v2} } 
[inproceedings] bibtexS. Linker and M. Hilscher, "Proof theory of a multilane spatial logic," in Proc. Theoretical Aspects of ComputingICTAC 2013, 2013, pp. 231248.
@inproceedings{LH13, title = {Proof theory of a multilane spatial logic},
author = {Linker, Sven and Hilscher, Martin},
booktitle = {Theoretical Aspects of ComputingICTAC 2013},
pages = {231248},
year = {2013},
publisher = {Springer} } 
[inproceedings] bibtex  Go to documentB. Engelmann, "Towards Practical Verification of Dynamically Typed Programs," in Proc. 25th Nordic Workshop on Programming Theory, 2013.
@inproceedings{Eng2013,
author = {Bj{\"o}rn Engelmann},
title = {Towards Practical Verification of Dynamically Typed Programs},
booktitle = {25th Nordic Workshop on Programming Theory},
year = {2013},
abstract = {Dynamically typed languages enable programmers to write elegant, reusable and extendable programs. Recently, some progress has been made regarding their verification. However, the user is currently required to manually show the absence of type errors, a tedious task usually involving large amounts of repetitive work. As most dynamically typed programs only occasionally divert from what would also be possible in statically typed languages, properly designed type inference algorithms should be able to supply the missing type information in most cases. We propose integrating a certified type inference algorithm into an interactive verification environment in order to a) provide a layer of abstraction, allowing the users to verify their programs like in a statically typed language whenever possible and b) use verification results to improve type inference and thus allow type checking of difficult cases.},
pdf = {http://theoretica.informatik.unioldenburg.de/~ben/papers/nwpt2013paper.pdf},
slides = {http://theoretica.informatik.unioldenburg.de/~ben/slides/nwpt2013/},
url = {http://theoretica.informatik.unioldenburg.de/~ben/papers/nwpt2013paper.pdf} } 
[inproceedings] bibtexM. Hilscher, S. Linker, and E. R. Olderog, "Proving Safety of Traffic Manoeuvres on Country Roads," in Proc. Theories of Programming and Formal Methods, 2013, pp. 196212.
@inproceedings{HLO13,
author = {M. Hilscher and S. Linker and E.R. Olderog},
editor = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
title = {Proving Safety of Traffic Manoeuvres on Country Roads},
booktitle = {Theories of Programming and Formal Methods},
publisher = {Springer},
series = {LNCS},
volume = {8051},
year = {2013},
pages = {196212} } 
[inproceedings] bibtex  Go to documentS. Kemper and C. Etzien, "A Visual Logic for the Description of Highway Traffic Scenarios," in Proc. Complex Systems Design & Management, Proceedings of the Fourth International Conference on Complex Systems Design & Management CSD&M 2013, Paris, France, December 46, 2013, 2013, pp. 233245.
@inproceedings{DBLP:conf/csdm/KemperE13,
author = {Stephanie Kemper and Christoph Etzien},
title = {A Visual Logic for the Description of Highway Traffic Scenarios},
booktitle = {Complex Systems Design {\&} Management, Proceedings of the Fourth International Conference on Complex Systems Design {\&} Management CSD{\&}M 2013, Paris, France, December 46, 2013},
pages = {233245},
year = {2013},
url = {http://dx.doi.org/10.1007/9783319028125_17},
doi = {10.1007/9783319028125_17},
timestamp = {Sun, 08 Dec 2013 13:34:23 +0100},
biburl = {http://dblp.unitrier.de/rec/bib/conf/csdm/KemperE13},
bibsource = {dblp computer science bibliography, http://dblp.org} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and M. Swaminathan, "Structural Transformations for DataEnriched RealTime Systems," in Proc. Integrated Formal Methods (iFM), 2013, pp. 378393.
@inproceedings{OlderogSwaminathan13,
author = {E.R. Olderog and Mani Swaminathan},
title = {Structural Transformations for DataEnriched RealTime Systems},
editor = {Einar Broch Johnsen and Luigia Petre},
booktitle = {Integrated Formal Methods (iFM)},
volume = {7940},
series = {Lecture Notes in Computer Science},
pages = {378393},
publisher = {SpringerVerlag},
year = {2013},
url = {http://dx.doi.org/10.1007/9783642386138_26} } 
[article] bibtexK. R. Apt, F. S. de Boer, E. R. Olderog, and S. de Gouw, "Verification of objectoriented programs: A transformational approach," J Computer System Sciences, vol. 78, pp. 823852, 2012.
@article{ABOG12,
author = {K. R. Apt and F. S. de Boer and E.R. Olderog and S. de Gouw},
title = {Verification of objectoriented programs: A transformational approach},
journal = {J Computer System Sciences},
volume = {78},
number = {},
pages = {823852},
year = {2012},
optnote = {DOI information: 10.1016/j.jcss.2011.08.002} } 
[article] bibtexE. R. Olderog and R. Wilhelm, "Turing und die Verifikation," InformatikSpektrum, vol. 35, iss. 4, pp. 271279, 2012.
@article{OW12,
author = {E.R. Olderog and R. Wilhelm},
title = {Turing und die {Verifikation}},
journal = {InformatikSpektrum},
volume = {35},
number = {4},
pages = {271279},
year = {2012},
optnote = {Themenheft: Turing} } 
[article] bibtex  Go to documentM. Swaminathan, J. P. Katoen, and E. R. Olderog, "Layered Reasoning for randomized distributed algorithms," Formal Asp. Comput., vol. 24, iss. 46, pp. 477496, 2012.
@article{SwaminathanKatoenOlderog12,
author = {M. Swaminathan and J.P. Katoen and E.R. Olderog},
title = {Layered Reasoning for randomized distributed algorithms},
journal = {Formal Asp. Comput.},
volume = {24},
number = {46},
year = {2012},
pages = {477496},
url = {http://dx.doi.org/10.1007/s001650120231x} } 
[inproceedings] bibtexS. Linker, "Translating Structural Process Properties to Petri Net Markings," in Proc. Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), 2012, pp. 8291.
@inproceedings{Lin12,
author = {S. Linker},
title = {Translating Structural Process Properties to Petri Net Markings},
booktitle = {Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12)},
pages = {8291},
publisher = {IEEE Computer Society Conference Publishing Services},
year = {2012},
month = {June},
abstract = {We introduce a spatiotemporal logic PSTL defined on PiCalculus processes. This logic is especially suited to formulate properties in relation to the structural semantics of the PiCalculus due to Meyer, a representation of processes as Petri nets. To allow for the use of wellresearched verification techniques, we present a translation of a subset of PSTL to LTL on Petri nets. We further prove soundness of our translation.} } 
[inproceedings] bibtexE. R. Olderog, "Automatic Verification of RealTime Systems with Rich Data  An Overview," in Proc. Theory and Applications of Models of Computation (TAMC), 2012, pp. 8493.
@inproceedings{Old12,
author = {E.R. Olderog},
title = {Automatic Verification of RealTime Systems with Rich Data  An Overview},
booktitle = {Theory and Applications of Models of Computation (TAMC)},
editor = {Manindra Agrawal and S. Barry Cooper and Angsheng Li},
series = {LNCS},
volume = {7287},
pages = {8493},
publisher = {Springer},
year = {2012} } 
[inproceedings] bibtexT. Strazny and R. Meyer, "An Algorithmic Framework for Coverability in WellStructured Systems," in Proc. Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), 2012, pp. 173182.
@inproceedings{straznymeyer:2012:framework,
author = {T. Strazny and R. Meyer},
title = {An Algorithmic Framework for Coverability in WellStructured Systems},
booktitle = {Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12)},
year = {2012},
pages = {173182},
month = {June},
publisher = {IEEE Computer Society Conference Publishing Services},
abstract = {We generalize the backward algorithm for coverability in WSTS's to an algorithmic framework. The idea is to consider the predecessor computation, the witness function, and the processing order as parameters. On the theoretical side, we prove that every instantiation of the functions (that satisfies some requirements) still yields a decision procedure for coverability. On the practical side, we show that known optimizations like partial order reduction and pruning can be formulated in our framework. We also give a novel acceleration based instantiation. For wellknown classes of WSTS's (PN, PN+Transfer, LCS), we optimize the selection function inspired by $A^*$. We implemented our instantiations and comment on the data structures. Extensive experiments show that the new algorithms can compete with a stateoftheart tool: MIST2.},
note = {Best Paper Award of ACSD} } 
[article] bibtex  Go to documentS. Kemper, "SATbased verification for timed component connectors," Science of Computer Programming, vol. 77, iss. 7–8, pp. 779798, 2012.
@article{Kemper2012779,
author = {S. Kemper},
title = {SATbased verification for timed component connectors },
journal = {Science of Computer Programming },
year = {2012},
volume = {77},
pages = {779  798},
number = {7–8},
note = {(1) FOCLASA’09 (2) FSEN’09 },
abstract = {Componentbased software construction relies on suitable models underlying components, and in particular the coordinators which orchestrate component behaviour. Verifying correctness and safety of such systems amounts to model checking the underlying system model. The model checking techniques not only need to be correct (since system sizes increase), but also scalable and efficient. In this paper, we present a SATbased approach for bounded model checking of Timed Constraint Automata, which permits true concurrency in the timed orchestration of components. We present an embedding of bounded model checking into propositional logic with linear arithmetic. We define a product that is linear in the size of the system, and in this way overcome the state explosion problem to deal with larger systems. To further improve model checking performance, we show how to embed our approach into an extension of counterexample guided abstraction refinement with Craig interpolants. },
doi = {http://dx.doi.org/10.1016/j.scico.2011.02.003},
issn = {01676423},
keywords = {Timed constraint automata},
url = {http://www.sciencedirect.com/science/article/pii/S0167642311000499} } 
[techreport] bibtexJ. Quesel and A. Platzer, "Playing Hybrid Games with KeYmaera.," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 84, 2012.
@techreport{DBLP:conf/cade/QueselP12:TR,
author = {JanDavid Quesel and Andr{\'e} Platzer},
title = {Playing Hybrid Games with {KeYmaera}.},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {H3},
year = {2012},
month = {April},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 84, note = {ISSN: 18609821, http://www.avacs.org.},
abstract = { We propose a new logic, called differential dynamic game logic (dDGL), for expressing properties of parametric hybrid games, and develop a theorem prover for it. We give an operational and a modal semantics of dDGL and prove their equivalence. To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic(dL). We provide rules for extending the dL sequent proof calculus to handle the dDGL specifics. We have implemented dDGL in the theorem prover KeYmaera and consider a case study in which a robot plays a game against other agents in a factory automation scenario. },
access = {open},
bibtex = {atr084.bib},
pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_084.pdf} } 
[inproceedings] bibtexJ. Quesel and A. Platzer, "Playing Hybrid Games with KeYmaera.," in Proc. Automated Reasoning, Sixth International Joint Conference, IJCAR 2012, Manchester, UK, Proceedings, 2012, pp. 439453.
@inproceedings{DBLP:conf/cade/QueselP12,
author = {JanDavid Quesel and Andr{\'e} Platzer},
title = {Playing Hybrid Games with {KeYmaera}.},
booktitle = {Automated Reasoning, Sixth International Joint Conference, IJCAR 2012, Manchester, UK, Proceedings},
month = {June},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
publisher = {Springer},
volume = {7364},
series = {LNCS},
pages = {439453},
doi = {10.1007/9783642313653_34},
pdf = {http://csd.informatik.unioldenburg.de/~jdq/paper/cdglijcar.pdf},
slides = {http://csd.informatik.unioldenburg.de/~jdq/slides/ijcar20120626.pdf},
note = {The original publication is available at \url{http://www.springerlink.com/content/l44k5x507h67737q}{www.springerlink.com}.},
keywords = {differential dynamic logic, hybrid games, sequent calculus, theorem proving, logics for hybrid systems, factory automation},
abstract = { We propose a new logic, called differential dynamic game logic (dDGL), for expressing properties of parametric hybrid games, and develop a theorem prover for it. We give an operational and a modal semantics of dDGL and prove their equivalence. To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic(dL). We provide rules for extending the dL sequent proof calculus to handle the dDGL specifics. We have implemented dDGL in the theorem prover KeYmaera and consider a case study in which a robot plays a game against other agents in a factory automation scenario. } } 
[article] bibtex  Go to documentJ. Faber, S. Linker, E. Olderog, and J. Quesel, "Syspect  Modelling, Specifying, and Verifying RealTime Systems with Rich Data," International Journal of Software and Informatics, vol. 5, iss. 12, pp. 117137, 2011.
@article{FLO+2011,
author = {Johannes Faber and Sven Linker and ErnstR{\"u}diger Olderog and JanDavid Quesel},
title = {Syspect  Modelling, Specifying, and Verifying RealTime Systems with Rich Data},
journal = {International Journal of Software and Informatics},
year = {2011},
volume = {5},
number = {12},
part = {1},
pages = {117137},
note = {ISSN 16737288.},
url = {http://www.ijsi.org/IJSI/ch/reader/create_pdf.aspx?file_no=i78&flag=1&journal_id=ijsi},
abstract = {We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous realtime constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSPOZDC of CSP (Communicating Sequential Processes), OZ (ObjectZ) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool HPILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect. },
publists = {syspect} } 
[inproceedings] bibtexT. Strazny, "Accelerating Backward Reachability Analysis," in Proc. Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11), 2011, pp. 24.
@inproceedings{strazny:2011:accelerating,
author = {Tim Strazny},
title = {Accelerating Backward Reachability Analysis},
booktitle = {Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11)},
year = {2011},
editor = {Paul Pettersson and Cristina Seceleanu},
pages = {24},
month = {October},
organization = {M\"{a}lardalen University Sweden},
note = {Technical report 254/2011},
abstract = {In the context of depthfirst backward reachability analysis, we identify two general operations which allow for performance improvements, while covering wellknown techniques such as partial order methods and pruning. We instantiate these operations with novel \emph{backward acceleration} techniques and employ methods of \emph{guided search} in this context. Further, we introduce \emph{supportbased search trees},
a data structure to represent upwardclosed sets (ucs's) which allows for efficient implementation of operations necessary for the analysis.},
comment = {M\"{a}lardalen RealTime Research Centre, Box 883, 72123 V\"{a}ster\r{a}s, Sweden},
issn = {14043041} } 
[techreport] bibtexB. Wirtz, T. Strazny, J. Rakow, and A. Rakow, "A Lane Change Assistance System: Cooperation and Hybrid Control," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 78, 2011.
@techreport{atr078,
author = {Boris Wirtz and Tim Strazny and Jan Rakow and Astrid Rakow},
title = {A Lane Change Assistance System: Cooperation and Hybrid Control},
institution = {SFB/TR 14 AVACS},
year = {2011},
type = {Reports of SFB/TR 14 AVACS},
number = {78},
month = {July},
note = {ISSN: 18609821, http://www.avacs.org},
abstract = { Automated Highway Systems (AHS's) are considered as a key technology that promises increased safety, reduced energy consumption and optimized traffic flow. Safe and dependable operation of AHS's is of paramount importance and requires the application of rigid formal methods at design time. In this report we present a model for a lane change assistance system which is meant to serve as a foundation for benchmarks boosting theoretic and algorithmic advances in formal verification of the challenging class of cyberphysical systems. The assistance system implements an autonomous lane change manoeuvre conducted in cooperation with other communicating agents. The model implements a layered design for traffic agents where aspects of communication and autonomous control are described as realtime and hybrid systems, respectively, which are intertwined by synchronous message passing. },
editor = {Bernd Becker and Werner Damm and Bernd Finkbeiner and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski},
series = {ATR},
subproject = {H3} } 
[inproceedings] bibtexJ. D. Quesel, M. Fränzle, and W. Damm, "Crossing the bridge between similar games," in Proc. Formal Modeling and Analysis of Timed Systems  9th International Conference (FORMATS), Aalborg, Denmark, 2123 September, 2011. Proceedings, 2011, pp. 160176.
@inproceedings{AVACSH3BRG11,
author = {J.D. Quesel AND M. Fr\"{a}nzle AND W. Damm},
title = {Crossing the bridge between similar games},
booktitle = {Formal Modeling and Analysis of Timed Systems  9th International Conference (FORMATS), Aalborg, Denmark, 2123 September, 2011. Proceedings},
year = {2011},
editor = {Stavros Tripakis and Uli Fahrenberg},
series = {LNCS},
volume = {6919},
pages = {160176},
month = {Sep.},
publisher = {Springer},
note = {The original publication is available at \url{http://www.springerlink.com/content/e6r94n5820k08626}{www.springerlink.com}.},
subproject = {H3},
pdf = {http://csd.informatik.unioldenburg.de/~jdq/paper/bridging.pdf},
slides = {http://csd.informatik.unioldenburg.de/~jdq/slides/bridgingformats20110921.pdf},
abstract = { Specifications and implementations of complex physical systems tend to differ as low level effects such as sampling are often ignored when high level models are created. Thus, the low level models are often not exact refinements of the high level specification. However, they are similar to those. To bridge the gap between those models, we study robust simulation relations for hybrid systems. We identify a family of robust simulation relations that allow for certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of simulation a broad class of logical properties is preserved. The question whether two systems are in simulation relation can be reduced to a reach avoid problem for hybrid games. We provide a sufficient condition under which a winning strategy for these games exists.} } 
[inproceedings] bibtex  Go to documentM. Hilscher, S. Linker, E. R. Olderog, and A. P. Ravn, "An Abstract Model for Proving Safety of MultiLane Traffic Manoeuvres," in Proc. Int'l Conf.\ on Formal Engineering Methods (ICFEM), 2011, pp. 404419.
@inproceedings{avacsh3dec11,
author = {M. Hilscher AND S. Linker AND E.R. Olderog AND A.P. Ravn},
title = {An Abstract Model for Proving Safety of MultiLane Traffic Manoeuvres},
booktitle = {Int'l Conf.\ on Formal Engineering Methods (ICFEM)},
year = {2011},
editor = {Shengchao Qin AND Zongyan Qiu},
volume = {6991},
series = {Lecture Notes in Computer Science},
pages = {404419},
month = {Oct.},
publisher = {SpringerVerlag},
note = {The original publication is available at \url{http://www.springerlink.com/content/y4721k1525v23520}{www.springerlink.com}.},
subproject = {H3},
pdf = {http://csd.informatik.unioldenburg.de/pub/Papers/hlor2011icfem.pdf},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hlor2011icfem.pdf},
abstract = { We present an approach to prove safety (collision freedom) of multilane motorway trac with lanechange manoeuvres. This is ultimately a hybrid veri cation problem due to the continuous dynamics of the cars. We abstract from the dynamics by introducing a new spatial interval logic based on the view of each car. To guarantee safety, we present two variants of a lanechange controller, one with perfect knowledge of the safety envelopes of neighbouring cars and one which takes only the size of the neighbouring cars into account. Based on these controllers we provide a local safety proof for unboundedly many cars by showing that at any moment the reserved space of each car is disjoint from the reserved space of any other car. } } 
[article] bibtexS. Fröschle, P. Janvcar, S. Lasota, and Z. Sawa, "Noninterleaving bisimulation equivalences on Basic Parallel Processes," Inf. Comput., vol. 208, iss. 1, pp. 4262, 2010.
@article{FrJaLaSa:InfComput10,
author = {Fr\"{o}schle, Sibylle and Jan\v{c}ar, Petr and Lasota, Slawomir and Sawa, Zden\v{e}k},
title = {Noninterleaving bisimulation equivalences on Basic Parallel Processes},
journal = {Inf. Comput.},
volume = {208},
number = {1},
year = {2010},
pages = {4262},
publisher = {Academic Press, Inc.} } 
[book] bibtex  Go to documentA. Platzer, Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Heidelberg: Springer, 2010.
@book{Platzer10,
author = {Andr{\'e} Platzer},
title = {Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics},
publisher = {Springer},
address = {Heidelberg},
year = {2010},
isbn = {9783642145094},
doi = {10.1007/9783642145094},
url = {http://symbolaris.com/lahs/} } 
[inproceedings] bibtexH. Baumgartner, M. Gieseking, C. Concolato, and J. L. Feuvre, "Individual Supportive Audio Signal Processing," in Proc. 26th Tonmeistertagung  VDT International Convention, Leipzig, Germany, 2010, pp. 282284.
@inproceedings{bauGieConFeu10,
author = {Hannah Baumgartner and Manuel Gieseking and Cyril Concolato and Jean Le Feuvre},
title = {Individual Supportive Audio Signal Processing},
publisher = {Verband Deutscher Tonmeister e.V.},
booktitle = {26th Tonmeistertagung  VDT International Convention},
month = {Nov.},
year = {2010},
pages = {282284},
address = {Leipzig, Germany} } 
[inproceedings] bibtexJ. Hoenicke, E. R. Olderog, and A. Podelski, "Fairness for Dynamic Control," in Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2010, pp. 251265.
@inproceedings{HOP10,
author = {J. Hoenicke and E.R. Olderog and A. Podelski},
title = {Fairness for Dynamic Control},
editor = {J. Esparza and R. Majumdar },
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS) },
series = {Lecture Notes in Computer Science},
volume = {6015},
publisher = {SpringerVerlag},
pages = {251265},
year = {2010} } 
[inproceedings] bibtexE. R. Olderog and A. Podelski, "Explicit Fair Scheduling for Dynamic Control," in Proc. Concurrency, Compositionality, and Correctness, 2010, pp. 96117.
@inproceedings{OlPo10,
author = {E.R. Olderog and A. Podelski},
editor = {D. Dams and U. Hannemann and M. Steffen},
title = { Explicit Fair Scheduling for Dynamic Control },
booktitle = {Concurrency, Compositionality, and Correctness },
series = {Lecture Notes in Computer Science},
volume = {5930 },
publisher = {SpringerVerlag },
pages = {96117 },
year = {2010} } 
[inproceedings] bibtex  Go to documentJ. Hoenicke, R. Meyer, and E. R. Olderog, "Kleene, Rabin, and Scott Are Available," in Proc. CONCUR 2010  Concurrency Theory (CONCUR), 2010, pp. 462477.
@inproceedings{HMO10,
author = {J. Hoenicke and R. Meyer and E.R. Olderog},
title = {Kleene, Rabin, and Scott Are Available},
editor = {Paul Gastin and Fran\c{c}ois Laroussinie},
booktitle = {CONCUR 2010  Concurrency Theory (CONCUR)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6269},
pages = {462477},
year = {2010},
url = {http://dx.doi.org/10.1007/9783642153754_32} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and M. Swaminathan, "Layered Composition for Timed Automata," in Proc. Formal Modeling and Analysis of Timed Systems (FORMATS), 2010, pp. 228242.
@inproceedings{OS10,
author = {E.R. Olderog and M. Swaminathan},
title = {Layered Composition for Timed Automata},
editor = {K. Chatterjee and T. A Henzinger},
booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS) },
series = {Lecture Notes in Computer Science},
volume = {6246},
publisher = {SpringerVerlag},
pages = {228242},
year = {2010},
url = {http://dx.doi.org/10.1007/9783642152979_18} } 
[inproceedings] bibtex  Go to documentS. Kemper, "Compositional Construction of RealTime Dataflow Networks," in Proc. Coordination Models and Languages, 12th International Conference, COORDINATION 2010, Amsterdam, The Netherlands, June 79, 2010. Proceedings, 2010, pp. 92106.
@inproceedings{Kem10,
author = {Stephanie Kemper},
editor = {Dave Clarke and Gul A. Agha},
title = {Compositional Construction of RealTime Dataflow Networks},
booktitle = {Coordination Models and Languages, 12th International Conference, COORDINATION 2010, Amsterdam, The Netherlands, June 79, 2010. Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6116},
year = {2010},
pages = {92106},
doi = {10.1007/9783642134142_7},
url = {http://csd.informatik.unioldenburg.de/~stephie/Kemper_COORDINATION10.pdf} } 
[inproceedings] bibtexR. Meyer and T. Strazny, "Petruchio: From dynamic networks to nets," in Proc. Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010, 2010, pp. 175179.
@inproceedings{MS2010, editor = {Tayssir Touili and Byron Cook and Paul Jackson},
volume = {6174},
year = {2010},
pages = {175179},
isbn = {9783642142949},
author = {R. Meyer and T. Strazny},
title = {Petruchio: From dynamic networks to nets},
booktitle = {Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010},
series = {LNCS},
publisher = {SpringerVerlag},
publists = {rmeyer},
abstract = {We introduce Petruchio, a tool for computing Petri net translations of dynamic networks. To cater for unbounded architectures beyond the capabilities of existing implementations, the principle fixedpoint engine runs interleaved with coverability queries. We discuss algorithmic enhancements and provide experimental evidence that Petruchio copes with models of reasonable size.} } 
[incollection] bibtex  Go to documentS. Linker, "Diagrammatic Specification of Mobile RealTime Systems," in Diagrammatic Representation and Inference, Goel, A., Jamnik, M., and Narayanan, N., Eds., Springer Berlin / Heidelberg, 2010, vol. 6170, pp. 316318.
@incollection{springerlink:10.1007/9783642146008_40,
author = {Linker, Sven},
affiliation = {Carl von Ossietzky University of Oldenburg},
title = {Diagrammatic Specification of Mobile RealTime Systems},
booktitle = {Diagrammatic Representation and Inference},
series = {Lecture Notes in Computer Science},
editor = {Goel, Ashok and Jamnik, Mateja and Narayanan, N.},
publisher = {Springer Berlin / Heidelberg},
isbn = {},
pages = {316318},
volume = {6170},
url = {http://dx.doi.org/10.1007/9783642146008_40},
note = {10.1007/9783642146008_40},
year = {2010} } 
[inproceedings] bibtexJ. Faber, C. Ihlemann, S. Jacobs, and V. SofronieStokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies," in Proc. Integrated Formal Methods, 2010, pp. 152167.
@inproceedings{FIJ+2010,
author = {J. Faber and C. Ihlemann and S. Jacobs and V. SofronieStokkermans},
title = {Automatic Verification of Parametric Specifications with Complex Topologies},
series = {Lecture Notes in Computer Science},
booktitle = {Integrated Formal Methods},
year = {2010},
editor = {D. M{\'e}ry and S. Merz},
volume = {6396},
pages = {152167},
publisher = {Springer, Heidelberg},
abstract = {The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSPOZDC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.},
pdf = {http://csd.informatik.unioldenburg.de/~jfaber/dl/IFM2010b.pdf},
note = {This publication is available at \url{http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/9783642162657_12} {SpringerLink}},
doi = {http://dx.doi.org/10.1007/9783642162657_12} } 
[inproceedings] bibtexJ. Faber, "Verification Architectures: Compositional Reasoning for Realtime Systems," in Proc. Integrated Formal Methods, 2010, pp. 136151.
@inproceedings{Faber2010,
author = {J. Faber},
title = {{Verification Architectures}: Compositional Reasoning for Realtime Systems},
booktitle = {Integrated Formal Methods},
year = {2010},
editor = {D. M{\'e}ry and S. Merz},
volume = {6396},
series = {Lecture Notes in Computer Science},
pages = {136151},
publisher = {Springer, Heidelberg},
doi = {10.1007/9783642162657_11},
abstract = { We introduce a conceptual approach to decompose realtime systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local realtime assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a realtime logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSPOZDC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification. },
pdf = {http://csd.informatik.unioldenburg.de/~jfaber/dl/IFM2010a.pdf},
note = {This publication is available at \url{http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/9783642162657_11} {SpringerLink}} } 
[techreport] bibtex  Go to documentJ. Faber, C. Ihlemann, S. Jacobs, and V. SofronieStokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 66, 2010.
@techreport{FIJS2010,
author = {Johannes Faber and Carsten Ihlemann and Swen Jacobs and Viorica SofronieStokkermans},
title = {Automatic Verification of Parametric Specifications with Complex Topologies},
institution = {SFB/TR 14 AVACS},
year = {2010},
type = {Reports of SFB/TR 14 AVACS},
number = {66},
note = {ISSN: 18609821, \url{http://www.avacs.org}{http://www.avacs.org}.},
abstract = {The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSPOZDC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.},
access = {open},
bibtex = {atr066.bib},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
series = {ATR},
subproject = {R1},
url = {http://csd.informatik.unioldenburg.de/~jfaber/dl/ATR066.pdf},
publists = {syspect} } 
[techreport] bibtex  Go to documentJ. Faber, "Verification Architectures: Compositional Reasoning for Realtime Systems," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 65, 2010.
@techreport{Faber2010a,
author = {J. Faber},
title = {Verification {A}rchitectures: Compositional Reasoning for Realtime Systems},
institution = {SFB/TR 14 AVACS},
year = {2010},
type = {Reports of SFB/TR 14 AVACS},
number = {65},
month = {August},
note = {ISSN: 18609821, \url{http://www.avacs.org}{http://www.avacs.org}.},
abstract = { We introduce a conceptual approach to decompose realtime systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local realtime assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a realtime logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSPOZDC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification. },
access = {open},
bibtex = {atr065.bib},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
series = {ATR},
subproject = {R1},
url = {http://csd.informatik.unioldenburg.de/~jfaber/dl/ATR065.pdf} } 
[article] bibtexS. B. Fröschle and D. Gorla, "Proceedings 16th International Workshop on Expressiveness in Concurrency," CoRR, vol. abs/0911.3189, 2009.
@article{FrGo:Express09,
author = {Sibylle B. Fr{\"o}schle and Daniele Gorla},
title = {Proceedings 16th International Workshop on Expressiveness in Concurrency},
journal = {CoRR},
volume = {abs/0911.3189},
year = {2009} } 
[article] bibtexS. Fröschle and G. Steel, "Analysing PKCS\#11 Key Management APIs with Unbounded Fresh Data," , pp. 92106, 2009.
@article{FrSt:ArspaWits09,
author = {Fr\"{o}schle, Sibylle and Steel, Graham},
title = {Analysing PKCS\#11 Key Management APIs with Unbounded Fresh Data},
book = {Foundations and Applications of Security Analysis: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPAWITS 2009, York, UK, March 2829, 2009, Revised Selected Papers},
year = {2009},
pages = {92106},
publisher = {SpringerVerlag} } 
[inproceedings] bibtexW. Czerwi'nski, S. Fröschle, and S. Lasota, "PartiallyCommutative ContextFree Processes," in Proc. CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory, 2009, pp. 259273.
@inproceedings{CzFrLa:Concur09,
author = {Czerwi\'{n}ski, Wojciech and Fr\"{o}schle, Sibylle and Lasota, S\lawomir},
title = {PartiallyCommutative ContextFree Processes},
booktitle = {CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory},
year = {2009},
pages = {259273},
publisher = {SpringerVerlag} } 
[article] bibtexS. Fröschle and S. Lasota, "Normed Processes, Unique Decomposition, and Complexity of Bisimulation Equivalences," Electron. Notes Theor. Comput. Sci., vol. 239, pp. 1742, 2009.
@article{FrLa:Infinity06,
author = {Fr\"{o}schle, Sibylle and Lasota, S\lawomir},
title = {Normed Processes, Unique Decomposition, and Complexity of Bisimulation Equivalences},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {239},
year = {2009},
pages = {1742},
publisher = {Elsevier Science Publishers B. V.} } 
[book] bibtex  Go to documentK. R. Apt, F. S. de Boer, and E. R. Olderog, Verification of Sequential and Concurrent Programs, 3rd Edition, SpringerVerlag, 2009.
@book{ABO09Book3,
author = { K. R. Apt and F. S. de Boer and E.R. Olderog },
title = {Verification of Sequential and Concurrent Programs, 3rd Edition},
series = {Texts in Computer Science},
publisher = {SpringerVerlag},
year = {2009},
note = {502 pp, ISBN 9781848827448},
url = {http://www.springer.com/computer/theoretical+computer+science/book/9781848827448} } 
[article] bibtexS. Fröschle, "Adding Branching to the Strand Space Model," Electron. Notes Theor. Comput. Sci., vol. 242, iss. 1, pp. 139159, 2009.
@article{Fr:Express08,
author = {Fr\"{o}schle, Sibylle},
title = {Adding Branching to the Strand Space Model},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {242},
number = {1},
year = {2009},
pages = {139159},
publisher = {Elsevier Science Publishers B. V.} } 
[inproceedings] bibtexE. R. Olderog and R. Meyer, "Automatatheoretic verification based on counterexample specification," in Proc. Informatik als Dialog zwischen Theorie und Anwendung, 2009, pp. 217225.
@inproceedings{erorm09,
author = {E.R. Olderog and R. Meyer},
title = {Automatatheoretic verification based on counterexample specification},
editor = {V. Diekert and K. Weicker and N. Weicker},
booktitle = {Informatik als Dialog zwischen Theorie und Anwendung},
year = {2009},
pages = {217225},
publisher = {ViewegTeubner},
publists = {rmeyer} } 
[article] bibtex  Go to documentS. Kemper, "SATbased Verification for Timed Component Connectors," Electr. Notes Theor. Comput. Sci., vol. 255, pp. 103118, 2009.
@article{Kem09,
author = {Stephanie Kemper},
title = {{SAT}based {V}erification for {T}imed {C}omponent {C}onnectors},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {255},
year = {2009},
pages = {103118},
url = {http://csd.informatik.unioldenburg.de/~stephie/Kemper_FOCLASA09.pdf},
doi = {10.1016/j.entcs.2009.10.027},
keywords = {Timed Constraint Automata, Abstraction Refinement, Model Checking, SAT, ComponentBased Software Engineering} } 
[inproceedings] bibtex  Go to documentM. Fränzle and M. Swaminathan, "Revisiting Decidability and Optimum Reachability for MultiPriced Timed Automata," in Proc. Formal Modeling and Analysis of Timed Systems (FORMATS), 2009, pp. 149163.
@inproceedings{MS09,
author = {M. Fr{\"a}nzle and M. Swaminathan},
title = {Revisiting Decidability and Optimum Reachability for MultiPriced Timed Automata},
editor = {J. Ouaknine and F. Vaandrager},
booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS) },
series = {Lecture Notes in Computer Science},
volume = {5813},
publisher = {SpringerVerlag},
pages = {149163},
year = {2009},
url = {http://dx.doi.org/10.1007/9783642043680_13} } 
[inproceedings] bibtexA. Schäfer and M. John, "Conceptional Modeling and Analysis of SpatioTemporal Processes in Biomolecular Systems," in Proc. Sixth AsiaPacific Conference on Conceptual Modelling (APCCM 2009), Wellington, New Zealand, January 2009, 2009, pp. 3948.
@inproceedings{sj09,
author = {Sch\"afer, A. and John, M.},
title = {Conceptional Modeling and Analysis of SpatioTemporal Processes in Biomolecular Systems},
booktitle = {Sixth AsiaPacific Conference on Conceptual Modelling (APCCM 2009), Wellington, New Zealand, January 2009},
editor = {Markus Kirchberg and Sebastian Link},
series = {CRPIT},
volume = {96},
publisher = {Australian Computer Society},
year = {2009},
pages = {3948},
publists = {schaefer} } 
[article] bibtexR. Meyer, V. Khomenko, and T. Strazny, "A Practical Approach to Verification of Mobile Systems Using Net Unfoldings," Fundamenta Informaticae, vol. 94, iss. 34, pp. 439471, 2009.
@article{MeyerKhomenkoStrazny2009Unfolding,
author = {R. Meyer and V. Khomenko and T. Strazny},
title = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
journal = {Fundamenta Informaticae},
publisher = {IOS Press},
note = {Special Issue on Petri Nets 2008, invited version of the ATPN 2008 paper},
volume = {94},
number = {34},
pages = {439471},
year = {2009},
publists = {rmeyer},
keywords = {finite control processes, safe processes, $\pi$Calculus, mobile systems, model checking, Petri net unfoldings},
abstract = { We propose a technique for verification of mobile systems. We translate \emph{finite control processes,} which are a wellknown subset of \picalc, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a nontrivial bound by static analysis. Moreover, we introduce the notion of \emph{safe processes,} which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfoldingbased verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system.} } 
[inproceedings] bibtex  Go to documentJ. Faber, "Verification Architectures for Realtime Systems," in Proc. Proceedings of Formal Methods 2009 Doctoral Symposium, 2009, pp. 1419.
@inproceedings{Faber2009,
author = {J. Faber},
title = {Verification Architectures for Realtime Systems},
booktitle = {Proceedings of Formal Methods 2009 Doctoral Symposium},
year = {2009},
editor = {M. Mousavi and E. Sekerinski},
number = {0915},
series = {CSReport, Eindhoven University of Technology},
pages = {1419},
pdf = {http://csd.informatik.unioldenburg.de/~jfaber/dl/FM09_DS.pdf},
url = {http://alexandria.tue.nl/repository/books/654108.pdf },
institution = {Eindhoven University of Technology},
type = {CSReport} } 
[inproceedings] bibtexA. Platzer, J. Quesel, and P. Rümmer, "Real World Verification," in Proc. Automated Deduction  CADE22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2  7, 2009, Proceedings, 2009, pp. 485501.
@inproceedings{DBLP:conf/cade/PlatzerQR09,
author = {Andr{\'e} Platzer and JanDavid Quesel and Philipp R{\"u}mmer},
title = {Real World Verification},
booktitle = {Automated Deduction  CADE22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2  7, 2009, Proceedings},
editor = {Renate A. Schmidt},
publisher = {Springer},
volume = {5663},
pages = {485501},
series = {LNCS},
year = {2009},
doi = {10.1007/9783642029592_35},
pdf = {http://symbolaris.com/pub/rwv.pdf},
note = {\url{http://dx.doi.org/10.1007/9783642029592_35}{(c) SpringerVerlag}},
abstract = {Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of realworld applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of realclosed fields: approaches based on quantifier elimination, Gr{\"o}bner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gr{\"o}bner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.} } 
[inproceedings] bibtexA. Platzer and J. Quesel, "European Train Control System: A Case Study in Formal Verification," in Proc. Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December 912, 2009, Proceedings, Heidelberg, 2009, pp. 246265.
@inproceedings{conf/icfem/PlatzerQ09,
author = {Andr{\'e} Platzer and JanDavid Quesel},
title = {European Train Control System: A Case Study in Formal Verification},
booktitle = {Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December 912, 2009, Proceedings},
editor = {Ana Cavalcanti and Karin Breitman},
publisher = {Springer},
address = {Heidelberg},
series = {LNCS},
volume = {5885},
pages = {246265},
year = {2009},
doi = {10.1007/9783642103735_13},
pdf = {http://symbolaris.com/pub/etcs.pdf},
slides = {http://csd.informatik.unioldenburg.de/~jdq/slides/ETCSslides.pdf},
note = {\url{http://dx.doi.org/10.1007/9783642103735_13}{(c) SpringerVerlag}},
abstract = {Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. Finally we verify that safety is preserved when a PI controller is used for speed supervision.} } 
[techreport] bibtexA. Platzer, J. Quesel, and P. Rümmer, "Real World Verification," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 52, 2009.
@techreport{DBLP:conf/cade/PlatzerQR09:TR,
author = {Andr{\'e} Platzer and JanDavid Quesel and Philipp R{\"u}mmer},
title = {Real World Verification},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {H3},
year = {2009},
month = {June},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 52, note = {ISSN: 18609821, http://www.avacs.org.},
access = {open},
abstract = {Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of realworld applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of realclosed fields: approaches based on quantifier elimination, Gr{\"o}bner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gr{\"o}bner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.},
bibtex = {atr052.bib},
pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_052.pdf} } 
[techreport] bibtexA. Platzer and J. Quesel, "European Train Control System: A Case Study in Formal Verification," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 54, 2009.
@techreport{conf/icfem/PlatzerQ09:TR,
author = {Andr{\'e} Platzer and JanDavid Quesel},
title = {European Train Control System: A Case Study in Formal Verification},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and ErnstR{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {H3},
year = {2009},
month = {Oct},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 54, note = {ISSN: 18609821, http://www.avacs.org.},
access = {open},
abstract = {Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. Finally we verify that safety is preserved when a PI controller is used for speed supervision.},
bibtex = {atr054.bib},
pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_054.pdf} } 
[book] bibtex  Go to documentE. R. Olderog and H. Dierks, RealTime Systems  Formal Specification and Automatic Verification  Errata: see below, Cambridge University Press, 2008.
@book{OD08,
author = {E.R. Olderog and H. Dierks},
title = {RealTime Systems  Formal Specification and Automatic Verification  Errata: see below},
publisher = {Cambridge University Press},
year = 2008, note = {ISBN 9780521883337. For more information see: \url{http://csd.informatik.unioldenburg.de/rtbook/}{http://csd.informatik.unioldenburg.de/rtbook/}},
url = {http://www.cambridge.org/de/academic/subjects/computerscience/distributednetworkedandmobilecomputing/realtimesystemsformalspecificationandautomaticverification} } 
[article] bibtexM. Möller, E. R. Olderog, H. Rasch, and H. Wehrheim, "Integrating a Formal Method into a Software Engineering Process with UML and Java," Formal Apsects of Computing, vol. 20, pp. 161204, 2008.
@article{MORW08,
author = {M. M{\"o}ller and E.R. Olderog and H. Rasch and H. Wehrheim},
title = {Integrating a Formal Method into a Software Engineering Process with {UML} and {Java}},
journal = {Formal Apsects of Computing},
year = {2008},
volume = {20},
pages = {161204},
abstract = {We describe how CSPOZ, a formal method combining the process algebra CSP with the specification language ObjectZ, can be integrated into an objectoriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed {\em reactive systems}. To this end, we propose a specific UML {\em profile} for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSPOZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for {\em verifying} properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating {\em contracts} for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by \CSPjassda{},
an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts.},
publists = {syspect} } 
[article] bibtexA. Platzer, "DifferentialAlgebraic Dynamic Logic for DifferentialAlgebraic Programs," Journal of Logic and Computation, 2008.
@article{DBLP:journals/logcom/Platzer08,
author = {Andr{\'e} Platzer},
title = {DifferentialAlgebraic Dynamic Logic for DifferentialAlgebraic Programs},
journal = {Journal of Logic and Computation},
year = {2008},
note = {Accepted for publication},
doi = {10.1093/logcom/exn070},
pdf = {http://symbolaris.com/pub/DAL.pdf},
keywords = {dynamic logic, differential constraints, sequent calculus, verification of hybrid systems, differential induction, theorem proving},
abstract = { We generalise dynamic logic to a logic for differentialalgebraic programs, i.e., discrete programs augmented with firstorder differentialalgebraic formulas as continuous evolution constraints in addition to firstorder discrete jump formulas. These programs characterise interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new \emph{differential induction} with which differentialalgebraic programs can be verified by exploiting their differential constraints algebraically without having to solve them. We develop the theory of differential induction and differential refinement and analyse their deductive power. As a case study, we present parametric tangential roundabout maneuvers in air traffic control and prove collision avoidance in our calculus.} } 
[inproceedings] bibtexM. Johns, B. Engelmann, and J. Posegga, "XSSDS: ServerSide Detection of CrossSite Scripting Attacks," in Proc. ACSAC, 2008, pp. 335344.
@inproceedings{JEP08,
author = {Martin Johns and Bj{\"o}rn Engelmann and Joachim Posegga},
title = {XSSDS: ServerSide Detection of CrossSite Scripting Attacks},
booktitle = {ACSAC},
year = {2008},
pages = {335344},
abstract = {Crosssite Scripting (XSS) has emerged to one of the most prevalent type of security vulnerabilities. While the reason for the vulnerability primarily lies on the serverside, the actual exploitation is within the victim's web browser on the clientside. Therefore, an operator of a web application has only very limited evidence of XSS issues. In this paper, we propose a passive detection system to identify successful XSS attacks. Based on a prototypical implementation, we examine our approach's accuracy and verify its detection capabilities. We compiled a dataset of 500.000 individual HTTP request/responsepairs from 95 popular web applications for this, in combination with both real word and manually crafted XSSexploits; our detection approach results in a total of zero false negatives for all tests, while maintaining an excellent false positive rate for more than 80\% of the examined web applications.},
bibtex = {jep08.bib},
doi = {10.1109/ACSAC.2008.36},
pdf = {http://www.acsac.org/openconf2008/modules/request.php?module=oc_proceedings&action=view.php&a=Accept&id=104} } 
[inproceedings] bibtex  Go to documentM. Swaminathan, M. Fränzle, and J. P. Katoen, "The Surprising Robustness of (Closed) Timed Automata against ClockDrift," in Proc. IFIP International Conference on Theoretical Computer Science (IFIP TCS), 2008, pp. 537553.
@inproceedings{SFK08,
author = {M. Swaminathan and M. Fr{\"a}nzle and J.P. Katoen},
title = {The Surprising Robustness of (Closed) Timed Automata against ClockDrift},
editor = {Giorgio Ausiello and Juhani Karhum{\"a}ki},
booktitle = {IFIP International Conference on Theoretical Computer Science (IFIP TCS) },
series = {International Federation for Information Processing},
volume = {273},
publisher = {Springer},
pages = {537553},
year = {2008},
url = {http://dx.doi.org/10.1007/9780387096803_36} } 
[techreport] bibtex  Go to documentV. Khomenko and R. Meyer, "Checking $\pi$Calculus Structural Congruence is Graph Isomorphism Complete," School of Computing Science, Newcastle University, CSTR: 1100, 2008.
@techreport{KhomenkoMeyer2008ComplexityStructCong,
author = {V. Khomenko and R. Meyer},
title = {Checking $\pi$Calculus Structural Congruence is Graph Isomorphism Complete},
number = {CSTR: 1100},
institution = {School of Computing Science, Newcastle University},
year = {2008},
note = {20 pages},
url = {http://www.cs.ncl.ac.uk/publications/trs/abstract/1100},
publists = {rmeyer},
keywords = {structural congruence, graph isomorphism, $\pi$Calculus, computational complexity},
abstract = {We show that the problems of checking $\pi$Calculus structural congruence ($\pi$SC) and graph isomorphism (GI) are Karp reducible to each other. The reduction from GI to $\pi$SC is given explicitly, and the reduction in the opposite direction proceeds by transforming $\pi$SC into an instance of the term equality problem (i.e., the problem of deciding equivalence of two terms in the presence of associative and/or commutative operations and commutative variablebinding quantifiers), which is known to be Karp reducible to GI. Our result is robust in the sense that it holds for several variants of structural congruence and some rather restrictive fragments of $\pi$Calculus. Furthermore, we address the question of solving $\pi$SC in practice, and describe a number of optimisations exploiting specific features of $\pi$Calculus terms, which allow one to significantly reduce the size of the resulting graphs that have to be checked for isomorphism.} } 
[techreport] bibtexR. Meyer, V. Khomenko, and T. Strazny, "A Practical Approach to Verification of Mobile Systems Using Net Unfoldings," School of Computing Science, Newcastle University, CSTR: 1064, 2008.
@techreport{MeyerKhomenkoStrazny2008UnfoldingTR,
author = {R. Meyer and V. Khomenko and T. Strazny},
title = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
institution = {School of Computing Science, Newcastle University},
month = {January},
year = {2008},
number = {CSTR: 1064},
note = {29 pages},
publists = {rmeyer},
keywords = {finite control processes, safe processes, $\pi$Calculus, mobile systems, model checking, Petri net unfoldings},
abstract = { In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a wellknown subset of $\pi$Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a nontrivial bound by static analysis. Moreover, we introduce the notion of safe pro cesses, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfoldingbased verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. } } 
[inproceedings] bibtexR. Meyer, V. Khomenko, and T. Strazny, "A Practical Approach to Verification of Mobile Systems Using Net Unfoldings," in Proc. Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008, 2008, pp. 327347.
@inproceedings{MeyerKhomenkoStrazny2008Unfolding,
author = {R. Meyer and V. Khomenko and T. Strazny},
title = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
booktitle = {Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008},
series = {LNCS},
volume = {5062},
publisher = {SpringerVerlag},
pages = {327347},
year = {2008},
publists = {rmeyer},
keywords = {finite control processes, safe processes, $\pi$Calculus, mobile systems, model checking, Petri net unfoldings},
abstract = { In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a wellknown subset of $\pi$Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a nontrivial bound by static analysis. Moreover, we introduce the notion of safe pro cesses, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfoldingbased verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime.} } 
[techreport] bibtexA. Platzer and E. M. Clarke, "Computing Differential Invariants of Hybrid Systems as Fixedpoints," School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, CMUCS08103, 2008.
@techreport{DBLP:conf/cav/PlatzerC08:TR,
author = {Andr{\'e} Platzer and Edmund M. Clarke},
title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints},
number = {CMUCS08103},
year = {2008},
month = {},
institution = {School of Computer Science, Carnegie Mellon University},
address = {Pittsburgh, PA},
annote = {Long version of~\cite{PlatzerC08}},
keywords = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine},
abstract = { We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations that have righthand sides that are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.},
pdf = {http://reportsarchive.adm.cs.cmu.edu/anon/2008/CMUCS08103.pdf} } 
[article] bibtexA. Platzer, "Differential Dynamic Logic for Hybrid Systems.," Journal of Automated Reasoning, vol. 41, iss. 2, pp. 143189, 2008.
@article{DBLP:journals/jar/Platzer08,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Hybrid Systems.},
journal = {Journal of Automated Reasoning},
year = {2008},
volume = {41},
number = {2},
pages = {143189},
doi = {10.1007/s1081700891038},
pdf = {http://symbolaris.com/pub/freedL.pdf},
note = {\url{http://dx.doi.org/10.1007/s1081700891038}{(c) SpringerVerlag}},
keywords = {dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems},
abstract = { Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of realvalued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is wellsuited for verifying realistic hybrid systems with parametric system dynamics. } } 
[article] bibtex  Go to documentA. Schäfer, "Beschreibung und Verifikation räumlicher und zeitlicher Eigenschaften mobiler Systeme," it  Information Technology, vol. 50, iss. 5, pp. 324326, 2008.
@article{schaefer2008,
author = {A. Sch\"afer},
title = {{Beschreibung und Verifikation r\"aumlicher und zeitlicher Eigenschaften mobiler Systeme}},
journal = {it  Information Technology},
year = {2008},
volume = {50},
pages = {324326},
number = {5},
doi = {DOI 10.1524/itit.2008.0503},
publists = {schaefer},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/itti0805_324a.pdf},
note = {\url{http://itInformationTechnology.de}{http://itInformationTechnology.de}},
abstract = { This paper provides an overview over a formal method for the analysis of mobile realtime systems. Control systems for cars and trains as well as mobile robots are examples of such systems. We develop a spatiotemporal logic that is used to model both the systems and safety requirements. We investigate the theoretical foundations like decidability and axiomatisability and develop a prototype tool for the automatic verification based on these results. The application of this logic is exemplified with an industrial case study.} } 
[inproceedings] bibtexR. Meyer, "On Boundedness in Depth in the $\pi$Calculus," in Proc. Proc. of the 5th IFIP International Conference on Theoretical Computer Science, IFIP TCS 2008, 2008.
@inproceedings{Meyer2008BoundedDepth,
author = {R. Meyer},
title = {On Boundedness in Depth in the $\pi$Calculus},
booktitle = {Proc. of the 5th IFIP International Conference on Theoretical Computer Science, IFIP TCS 2008},
series = {IFIP},
volume = {273},
publisher = {SpringerVerlag},
year = {2008},
pages = {},
note = {To appear},
publists = {rmeyer},
keywords = {$\pi$Calculus, structural congruence, wellstructured transition systems, termination},
abstract = { We investigate the class $P_{\mathit{BD}}$ of $\pi$Calculus processes that are bounded in the function depth. First, we show that boundedness in depth has an intuitive characterisation when we understand processes as graphs: a process is bounded in depth if and only if the length of the simple paths is bounded. The proof is based on a new normal form for the $\pi$Calculus called anchored fragments. Using this concept, we then show that processes of bounded depth have wellstructured transition systems (WSTS). As a consequence, the termination problem is decidable for this class of processes. The instantiation of the WSTS framework employs a new wellquasiordering for processes in $P_{\mathit{BD}}$.} } 
[inproceedings] bibtex  Go to documentA. Platzer and J. Quesel, "Logical Verification and Systematic Parametric Analysis in Train Control.," in Proc. Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings, 2008, pp. 646649.
@inproceedings{DBLP:conf/hybrid/PlatzerQ08,
author = {Andr{\'e} Platzer and JanDavid Quesel},
title = {Logical Verification and Systematic Parametric Analysis in Train Control.},
year = {2008},
pages = {646649},
doi = {10.1007/9783540789291_55},
editor = {Magnus Egerstedt and Bud Mishra},
booktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings},
publisher = {Springer},
series = {LNCS},
volume = {4981},
isbn = {},
keywords = {parametric verification, logic for hybrid systems, symbolic decomposition},
abstract = { We formally verify hybrid safety properties of cooperation protocols in a fully parametric version of the European Train Control System (ETCS). We present a formal model using hybrid programs and verify correctness using our logicbased decomposition procedure. This procedure supports free parameters and parameter discovery, which is required to determine correct design choices for free parameters of ETCS.},
url = {http://symbolaris.com/pub/ETCSshort.pdf},
note = {\url{http://dx.doi.org/10.1007/9783540789291_55}{(c) SpringerVerlag}} } 
[article] bibtex  Go to documentR. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko, "Model Checking Duration Calculus: A Practical Approach," Formal Aspects of Computing, vol. 20, iss. 45, pp. 481505, 2008.
@article{Meyer2008,
author = {R. Meyer and J. Faber and J. Hoenicke and A. Rybalchenko},
title = {Model Checking Duration Calculus: A Practical Approach},
journal = {Formal Aspects of Computing},
year = {2008},
publisher = {Springer London},
volume = {20},
pages = {481505},
number = {45},
month = jul, note = {{ISSN} 09345043 (Print) 1433299X (Online)},
abstract = {Model checking of realtime systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automatabased semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into subproperties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and realtime aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).},
doi = {10.1007/s0016500800827},
issn = {09345043},
keywords = {Model checking, Verification, Duration Calculus, Timed automata, Realtime systems, European Train Control System, Case study},
url = {http://www.springerlink.com/content/81g876074077601g/fulltext.pdf},
publists = {rmeyer,pea,syspect} } 
[inproceedings] bibtexA. Platzer and E. M. Clarke, "Computing Differential Invariants of Hybrid Systems as Fixedpoints," in Proc. ComputerAided Verification, CAV 2008, Princeton, USA, Proceedings, 2008, pp. 176189.
@inproceedings{DBLP:conf/cav/PlatzerC08,
author = {Andr{\'e} Platzer and Edmund M. Clarke},
title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints},
year = {2008},
month = {},
editor = {Aarti Gupta and Sharad Malik},
booktitle = {ComputerAided Verification, CAV 2008, Princeton, USA, Proceedings},
publisher = {Springer},
series = {LNCS},
pages = {176189},
volume = {5123},
isbn = {},
doi = {10.1007/9783540705451_17},
keywords = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine},
abstract = { We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose righthand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.},
pdf = {http://symbolaris.com/pub/fpdi.pdf},
note = {\url{http://dx.doi.org/10.1007/9783540705451_17}{(c) SpringerVerlag}} } 
[inproceedings] bibtex  Go to documentE. R. Olderog, "Automatic Verification of Combined Specifications," in Proc. Proc. of the 1st Internat. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2007), Macau, 2008, pp. 316.
@inproceedings{Old08,
author = {E.R. Olderog},
title = {Automatic Verification of Combined Specifications},
booktitle = {Proc. of the 1st Internat. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2007), Macau},
year = {2008},
editor = {G. Pu and V. Stolz},
series = {ENTCS},
journal = {Electr. Notes Theor. Comput. Sci.},
issn = {15710661},
volume = {207},
number = {},
month = {April},
pages = {316},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.03.082},
url = {},
keywords = {Realtime systems, complex data, CSP, ObjectZ, Duration Calculus, model checking, abstraction refinement, UML profile, tool support},
abstract = { This paper gives an overview of results of the project ``Beyond Timed Automata'' carried out in the Collaborative Research Center AVACS (Automatic Verification and Analysis of Complex Systems) of the Universities of Oldenburg, Freiburg, and Saarbr\"ucken. We discuss how properties of highlevel specifications of realtime systems combining the dimensions of process behaviour, data, and time can be automatically verified, exploiting recent advances in semantics, constraintbased model checking, and decision procedures for complex data. As specification language we consider CSOZDC, which integrates concepts from Communicating Sequential Processes (CSP), ObjectZ (OZ), and Duration Calculus (DC). Our approach to automatic verification of CSPOZDC rests on a compositional semantics of this languages in terms of PhaseEventAutomata. These can be translated into Transition Constraint Systems which serve as an input language of an abstract refinement model checker called ARMC which can handle constraints covering both realtime and infinite data. This is demonstrated by a case study concerning emergency messages in the European Train Control System (ETCS). For CSPOZDC we also discuss a UML profile and tool support. } } 
[inproceedings] bibtex  Go to documentA. Platzer and J. Quesel, "KeYmaera: A Hybrid Theorem Prover for Hybrid Systems.," in Proc. Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, 2008, pp. 171178.
@inproceedings{DBLP:conf/cade/PlatzerQ08,
author = {Andr{\'e} Platzer and JanDavid Quesel},
title = {{KeYmaera}: A Hybrid Theorem Prover for Hybrid Systems.},
booktitle = {Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings},
year = {2008},
pages = {171178},
editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
publisher = {Springer},
series = {LNCS},
volume = {5195},
doi = {10.1007/9783540710707_15},
isbn = {10.1007/9783540710707_15},
issn = {03029743},
keywords = {dynamic logic, automated theorem proving, decision procedures, computer algebra, verification of hybrid systems},
abstract = { KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which is a realvalued firstorder dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized freevariable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.},
note = {\url{http://dx.doi.org/10.1007/9783540710707_15}{(c) SpringerVerlag}},
url = {http://symbolaris.com/pub/KeYmaera.pdf},
slides = {http://csd.informatik.unioldenburg.de/~jdq/slides/keymaeraslides.pdf} } 
[inproceedings] bibtexS. Fröschle, "The Insecurity Problem: tackling Unbounded Data," in Proc. IEEE Computer Security Foundations Symposium 2007, 2007.
@inproceedings{Froeschle:CSF07,
author = {Sibylle Fr{\"o}schle},
title = {The Insecurity Problem: tackling Unbounded Data},
booktitle = {IEEE Computer Security Foundations Symposium 2007},
year = {2007},
publisher = {IEEE Computer Society},
abstract = { In this paper we focus on tackling the insecurity problem of security protocols in the presence of an unbounded number of data such as nonces or session keys. First, we pinpoint four open problems in this category. The first two problems concern protocols with natural restrictions that any `realistic' protocol should satisfy while the second two concern protocols with disequality constraints. For protocols with disequality constraints we will prove: (1)~Insecurity is decidable in NEXPTIME when bounding the size of messages and not requiring data to be \emph{freshly} generated. (2)~Insecurity is NEXPTIMEcomplete when bounding the size of messages and the number of freshly generated data used in honest sessions. This shows that unbounded data can be tackled in settings which do not trivially reduce to the case of bounded data. The second result is in contrast with a recently published proof, which appears to prove the same problem undecidable. We will point out why this proof cannot be considered to be valid. },
publists = {froeschle} } 
[inproceedings] bibtexR. Meyer, "A Petri Net Semantics for $\pi$Calculus Verification," in Proc. Dagstuhl ''zehn plus eins'', 2007, pp. 7677.
@inproceedings{Meyer2007Dagstuhl,
author = {R. Meyer},
title = {{A Petri Net Semantics for $\pi$Calculus Verification}},
booktitle = {Dagstuhl ''zehn plus eins''},
pages = {7677},
year = {2007},
publisher = {Verlagshaus Mainz GmbH Aachen},
publists = {rmeyer} } 
[article] bibtexS. Fröschle and S. l, "Causality versus trueconcurrency," Theoretical Computer Science, vol. 386, iss. 3, pp. 169187, 2007.
@article{FrLa:TCS07,
author = {Sibylle Fr{\"o}schle and S{\l}awomir Lasota},
title = {Causality versus trueconcurrency},
journal = {Theoretical Computer Science},
year = {2007},
volume = {386},
number = {3},
pages = {169187},
publists = {froeschle} } 
[article] bibtexB. Becker, A. Podelski, W. Damm, M. Fränzle, E. R. Olderog, and R. Wilhelm, "SFB/TR 14 AVACS  Automatic Verification and Analysis of Complex Systems," it  Information Technology, vol. 49, iss. 2, pp. 118126, 2007.
@article{AVACS07,
author = {B. Becker and A. Podelski and W. Damm and M. Fr{\"a}nzle and E.R. Olderog and R. Wilhelm},
title = {{SFB/TR 14 AVACS  Automatic Verification and Analysis of Complex Systems}},
journal = {it  Information Technology},
publisher = {Oldenbourg},
year = {2007},
number = {2},
volume = {49},
pages = {118126},
note = {See also \url{http://www.avacs.org}{http://www.avacs.org}} } 
[article] bibtexA. Schäfer, "Axiomatisation and Decidability of MultiDimensional Duration Calculus," TIME'05 special issue of Information and Computation, vol. 205, iss. 1, 2007.
@article{schaefer07,
author = {A. Sch\"afer},
title = {Axiomatisation and Decidability of MultiDimensional Duration Calculus},
journal = {TIME'05 special issue of Information and Computation},
year = {2007},
volume = {205},
number = {1},
note = {DOI \url{http://dx.doi.org/10.1016/j.ic.2006.08.005}{10.1016/j.ic.2006.08.005} },
publists = {schaefer},
abstract = { The Shape Calculus is a spatiotemporal logic based on an $n$dimensional Duration Calculus tailored for the specification and verification of mobile realtime systems. After showing nonaxiomatisability, we give a complete embedding in $n$dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use. } } 
[inproceedings] bibtexD. Basin, E. R. Olderog, and P. E. Sevinç, "Specifying and analyzing security automata using CSPOZ," in Proc. Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007), 2007, pp. 7081.
@inproceedings{BSO07,
author = {D. Basin and E.R. Olderog and P.E. Sevin\c{c}},
title = {Specifying and analyzing security automata using {CSPOZ}},
booktitle = {Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007)},
pages = {7081},
year = 2007, month = {March},
publisher = {ACM Press},
location = {Singapore},
abstract = { Security automata are a variant of B\"uchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSPOZ, a specification language combining Communicating Sequential Processes (CSP) and ObjectZ (OZ), to specify security automata, formalize their combination with target systems, and analyze the security of the resulting system specifications. We provide theoretical results relating CSPOZ specifications and security automata and show how refinement can be used to reason about specifications of security automata and their combination with target systems. Through a case study, we provide evidence for the practical usefulness of this approach. This includes the ability to specify concisely complex operations and complex control, support for structured specifications, refinement, and transformational design, as well as automated, toolsupported analysis. } } 
[article] bibtex  Go to documentA. Schäfer, "PhD Abstract: Specification and Verification of Mobile RealTime Systems," Bulletin of the EATCS, vol. 92, pp. 193195, 2007.
@article{sch07b,
author = {A. Sch\"afer},
title = {{PhD Abstract: Specification and Verification of Mobile RealTime Systems}},
editor = {V. Sassone},
year = {2007},
pages = {193195},
publisher = {EATCS},
journal = {Bulletin of the EATCS},
volume = {92},
publists = {schaefer},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/as07b.pdf} } 
[inproceedings] bibtex  Go to documentA. Schäfer, "Spezifikation und Verifikation mobiler Realzeitsysteme," in Proc. Ausgezeichnete Informatikdissertationen 2007, 2007, pp. 169177.
@inproceedings{sch07a,
author = {A. Sch\"afer},
title = {{Spezifikation und Verifikation mobiler Realzeitsysteme}},
booktitle = {{Ausgezeichnete Informatikdissertationen 2007}},
editor = {D. Wagner},
year = {2007},
pages = {169177},
series = {GIEditionLecture Notes in Informatics (LNI)},
publisher = {Gesellschaft f\"ur Informatik},
publists = {schaefer},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/as07a.pdf} } 
[techreport] bibtex  Go to documentA. Platzer, "A Temporal Dynamic Logic for Verifying Hybrid System Invariants.," , Reports of SFB/TR 14 AVACS 12, 2007.
@techreport{DBLP:conf/lfcs/Platzer07:TR,
author = {Andr{\'e} Platzer},
title = {A Temporal Dynamic Logic for Verifying Hybrid System Invariants.},
number = {12},
year = {2007},
month = {February},
editor = {B. Becker and W. Damm and M. Fr{\"a}nzle and E.R. Olderog and A. Podelski and R. Wilhelm},
optinstitution = {{SFB/TR~14 AVACS}},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
note = {ISSN: 18609821, http://www.avacs.org.},
url = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_012.pdf},
annote = {Long version of~\cite{DBLP:conf/lfcs/Platzer07}} } 
[inproceedings] bibtex  Go to documentJ. Faber, S. Jacobs, and V. SofronieStokkermans, "Verifying CSPOZDC Specifications with Complex Data Types and Timing Parameters," in Proc. Integrated Formal Methods, 2007, pp. 233252.
@inproceedings{FJSS07,
author = {J. Faber and S. Jacobs and V. SofronieStokkermans},
title = {Verifying {CSPOZDC} Specifications with Complex Data Types and Timing Parameters},
booktitle = {Integrated Formal Methods},
year = {2007},
editor = {J. Davies and J. Gibbons},
volume = {4591},
series = {Lecture Notes in Computer Science},
pages = {233252},
publisher = {SpringerVerlag},
month = jul, publists = {pea},
abstract = {We extend existing verification methods for CSPOZDC to reason about realtime systems with complex data types and timing parameters. We show that important properties of systems can be encoded in wellbehaved logical theories in which hierarchical reasoning is possible. Thus, testing invariants and bounded model checking can be reduced to checking satisfiability of ground formulae over a simple base theory. We illustrate the ideas by means of a simplified version of a case study from the European Train Control System standard.},
url = {http://csd.informatik.unioldenburg.de/~jfaber/dl/FaberJacobsSofronie.pdf} } 
[techreport] bibtex  Go to documentJ. Faber and I. Stierand, "From HighLevel Verification to RealTime Scheduling: A PropertyPreserving Integration," SFB/TR 14 AVACS, Reports of SFB/TR 14 AVACS 19, 2007.
@techreport{atr19,
author = {J. Faber and I. Stierand},
title = {From HighLevel Verification to RealTime Scheduling: A PropertyPreserving Integration},
editor = {B. Becker and W. Damm and M. Fr{\"a}nzle and E.R. Olderog and A. Podelski and R. Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {R1,R2},
year = {2007},
month = {June},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 19, note = {{ISSN} 18609821, \url{http://www.avacs.org}{http://www.avacs.org}.},
abstract = { In the design process of realtime systems, formal verification establishes global properties of highlevel specifications while realtime scheduling analysis ensures that concrete realisations meet essential timing properties with respect to a given target platform. But a formal link between these phases is missing. It is unclear (1) whether timing assumptions that are required to verify properties of highlevel specifications can actually be realised on a target platform and (2) whether verified properties remain valid for a schedulable task network. Our approach bridges this gap by guaranteeing that properties verified on specification level are preserved on the implementation level, and vice versa, schedulability results can be propagated back to the specification. To this end, we provide a propertypreserving translation from a subclass of the highlevel realtime language CSPOZDC into Cyclic Timed Automata, a Timed Automata based task network formalism. We apply our method to a case study from the European Train Control System standard. },
url = {http://csd.informatik.unioldenburg.de/~jfaber/dl/FaberStierand2007.pdf} } 
[inproceedings] bibtex  Go to documentA. Platzer and E. M. Clarke, "The Image Computation Problem in Hybrid Systems Model Checking.," in Proc. Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, 2007, pp. 473486.
@inproceedings{DBLP:conf/hybrid/PlatzerC07,
author = {Andr{\'e} Platzer and Edmund M. Clarke},
title = {The Image Computation Problem in Hybrid Systems Model Checking.},
year = {2007},
doi = {10.1007/9783540714934_37},
editor = {A. Bemporad and A. Bicchi and G. Buttazzo},
booktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings},
publisher = {SpringerVerlag},
series = {LNCS},
pages = {473486},
volume = {4416},
keywords = {model checking, hybrid systems, image computation},
note = {\url{http://dx.doi.org/10.1007/9783540714934_37}{(c) SpringerVerlag}},
url = {http://symbolaris.com/pub/happroximation.pdf},
abstract = { In this paper, we analyze limits of approximation techniques for (nonlinear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically even for a very restricted class of functions. Moreover, we show that symbolic insight about derivative bounds provides sufficient additional information for approximation refinement model checking. Finally, we prove that purely numerical algorithms can perform continuous image computation with arbitrarily high probability. Using these results, we analyze the prerequisites for a safe operation of the roundabout maneuver in air traffic collision avoidance. } } 
[inproceedings] bibtex  Go to documentA. Platzer, "A Temporal Dynamic Logic for Verifying Hybrid System Invariants.," in Proc. Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, 2007, pp. 457471.
@inproceedings{DBLP:conf/lfcs/Platzer07,
author = {Andr{\'e} Platzer},
title = {A Temporal Dynamic Logic for Verifying Hybrid System Invariants.},
editor = {S. Artemov and A. Nerode},
doi = {10.1007/9783540727347_32},
booktitle = {Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings},
publisher = {Springer},
series = {LNCS},
year = {2007},
pages = {457471},
volume = {4514},
note = {\url{http://dx.doi.org/10.1007/9783540727347_32}{(c) SpringerVerlag}},
url = {http://symbolaris.com/pub/dTL.pdf},
keywords = {dynamic logic, sequent calculus, logic for hybrid systems, temporal logic, deductive verification of embedded systems},
abstract = { We combine firstorder dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with firstorder definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to nontemporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints. } } 
[inproceedings] bibtex  Go to documentA. Platzer, "Combining Deduction and Algebraic Constraints for Hybrid System Analysis.," in Proc. 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, 2007, pp. 164178.
@inproceedings{DBLP:conf/verify/Platzer07,
author = {Andr{\'e} Platzer},
title = {Combining Deduction and Algebraic Constraints for Hybrid System Analysis.},
booktitle = {4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany},
year = {2007},
pages = {164178},
editor = {Bernhard Beckert},
volume = {259},
publisher = {CEURWS.org},
series = {},
note = {\url{http://ceurws.org/Vol259}{CEUR Workshop Proceedings}},
issn = {16130073},
keywords = {modular prover combination, analytic tableaux, verification of hybrid systems, dynamic logic},
abstract = { We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. In particular, we highlight the interaction of deductive and algebraic reasoning that is used for handling the joint discrete and continuous behaviour of hybrid systems. We illustrate proof tasks that occur when verifying scenarios with cooperative traffic agents. From the experience with these examples, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems, and we propose an iterative background closure strategy.},
url = {http://symbolaris.com/pub/cdachsa.pdf} } 
[inproceedings] bibtex  Go to documentS. Kemper and A. Platzer, "SATbased Abstraction Refinement for Realtime Systems," in Proc. Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, 2007, pp. 107122.
@inproceedings{DBLP:journals/entcs/KemperP07,
author = {Stephanie Kemper and Andr{\'e} Platzer},
title = {SATbased Abstraction Refinement for Realtime Systems},
booktitle = {Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings},
year = {2007},
editor = {Frank S. de Boer and Vladimir Mencl},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {182},
series = {ENTCS},
issn = {15710661},
pages = {107122},
doi = {10.1016/j.entcs.2006.09.034},
url = {http://symbolaris.com/pub/SAAtRe.pdf},
keywords = {abstraction refinement, model checking, realtime systems, SAT, Craig interpolation},
abstract = { In this paper, we present an abstraction refinement approach for model checking safety properties of realtime systems using SATsolving. With a faithful embedding of bounded model checking for systems of timed automata into propositional logic and linear arithmetic, we achieve both, quick abstraction techniques and a linearsize representation of parallel composition. In this logical setting, we introduce an abstraction that works uniformly for clocks, events, and states. When necessary, abstractions are refined by analysing spurious counterexamples using a promising extension of counterexampleguided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logicbased abstraction refinement. } } 
[inproceedings] bibtexW. Damm, A. Mikschl, J. Oehlerking, E. Olderog, J. Pang, A. Platzer, M. Segelken, and B. Wirtz, "Automating Verification of Cooperation, Control, and Design in Traffic Applications.," in Proc. Formal Methods and Hybrid RealTime Systems, 2007, pp. 115169.
@inproceedings{DammMOOPPSW07,
author = {Werner Damm and Alfred Mikschl and Jens Oehlerking and ErnstR{\"u}diger Olderog and Jun Pang and Andr{\'e} Platzer and Marc Segelken and Boris Wirtz},
title = {Automating Verification of Cooperation, Control, and Design in Traffic Applications.},
year = {2007},
pages = {115169},
editor = {Cliff Jones and Zhiming Liu and Jim Woodcock},
booktitle = {Formal Methods and Hybrid RealTime Systems},
publisher = {SpringerVerlag},
series = {LNCS},
volume = {4700},
doi = {10.1007/9783540752219_6},
issn = {},
keywords = {},
abstract = { We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of preverified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, modelchecking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.},
note = {\url{http://dx.doi.org/10.1007/9783540752219_6}{(c) SpringerVerlag}} } 
[inproceedings] bibtex  Go to documentI. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim, "Slicing Abstractions," in Proc. FSEN 2007: IPM International Symposium on Fundamentals of Software Engineering, 2007, pp. 1732.
@inproceedings{BDFW07,
author = {I. Br\"uckner and K. Dr\"ager and B. Finkbeiner and H. Wehrheim},
title = {{Slicing Abstractions}},
booktitle = {FSEN 2007: IPM International Symposium on Fundamentals of Software Engineering},
series = {Lecture Notes in Computer Science},
volume = {4767},
publisher = {Springer},
issn = {},
isbn = {9783540756972},
editor = {F. Arbab and M. Sirjani},
pages = {1732},
month = {April},
year = {2007},
abstract = { Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for infinitestate concurrent systems that interleaves automatic abstraction refinement, which splits states according to new predicates obtained by Craig interpolation, with slicing, which removes irrelevant states and transitions from the abstraction. The effects of abstraction and slicing complement each other. As the refinement progresses, the increasing accuracy of the abstract model allows for a more precise slice; the resulting smaller representation gives room for additional predicates in the abstraction. The procedure terminates when an error path in the abstraction can be concretized, which proves that the system is erroneous, or when the slice becomes empty, which proves that the system is correct. },
publists = {brueckner,wehrheim},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib07fsen.pdf} } 
[inproceedings] bibtex  Go to documentA. Platzer, "Differential Logic for Reasoning about Hybrid Systems.," in Proc. Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, 2007, pp. 746749.
@inproceedings{DBLP:conf/hybrid/Platzer07,
author = {Andr{\'e} Platzer},
title = {Differential Logic for Reasoning about Hybrid Systems.},
year = {2007},
optee = {},
editor = {A. Bemporad and A. Bicchi and G. Buttazzo},
booktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings},
publisher = {SpringerVerlag},
series = {LNCS},
pages = {746749},
doi = {10.1007/9783540714934_75},
volume = {4416},
note = {\url{http://dx.doi.org/10.1007/9783540714934_75}{(c) SpringerVerlag}},
url = {http://symbolaris.com/pub/dLshort.pdf},
keywords = {dynamic logic, hybrid systems, parametric verification},
abstract = { We propose a firstorder dynamic logic for reasoning about hybrid systems. As a uniform model for discrete and continuous evolutions in hybrid systems, we introduce hybrid programs with differential actions. Our logic can be used to specify and verify correctness statements about hybrid programs, which are suitable for symbolic processing by calculus rules. Using firstorder variables, our logic supports systems with symbolic parameters. With dynamic modalities, it is prepared to handle multiple system components. } } 
[inproceedings] bibtex  Go to documentA. Platzer, "Differential Dynamic Logic for Verifying Parametric Hybrid Systems.," in Proc. Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 36, 2007, Proceedings, 2007, pp. 216232.
@inproceedings{DBLP:conf/tableaux/Platzer07,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Verifying Parametric Hybrid Systems.},
pages = {216232},
doi = {10.1007/9783540730996_17},
keywords = {dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination},
abstract = { We introduce a firstorder dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and firstorder definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 36, 2007, Proceedings},
year = {2007},
editor = {Nicola Olivetti},
volume = {4548},
series = {LNCS},
publisher = {SpringerVerlag},
isbn = {},
note = {\url{http://dx.doi.org/10.1007/9783540730996_17}{(c) SpringerVerlag}},
url = {http://symbolaris.com/pub/dL.pdf} } 
[inproceedings] bibtex  Go to documentI. Brückner, "Slicing Concurrent RealTime System Specifications for Verification," in Proc. Integrated Formal Methods, 2007, pp. 5474.
@inproceedings{ib07ifm,
author = {I. Br{\"u}ckner},
title = {{Slicing Concurrent RealTime System Specifications for Verification}},
booktitle = {Integrated Formal Methods},
series = {Lecture Notes in Computer Science},
volume = {4591},
publisher = {SpringerVerlag},
issn = {03029743},
isbn = {9783540732099},
editor = {J. Davies and J. Gibbons},
pages = {5474},
month = jul, year = {2007},
abstract = { The highlevel specification language CSPOZDC has been shown to be wellsuited for modelling and analysing industrially relevant concurrent realtime systems. It allows to model each of the most important functional aspects such as control flow, data, and realtime requirements in adequate notations, maintaining a common semantical foundation for subsequent verification. Slicing on the other hand has become an established technique to complement the fight against state space explosion during verification which inherently accompanies increasing system complexity. In this paper, we exploit the special structure of CSPOZDC specifications by extending the dependence graphwhich usually serves as a basis for slicingwith several new types of dependencies, including timing dependencies derived from the specification's DC part. Based on this we show how to compute a specification slice and prove correctness of our approach. },
publists = {brueckner},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib07ifm.pdf} } 
[inproceedings] bibtex  Go to documentA. Platzer, "Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems," in Proc. Proc., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, 2007, pp. 6377.
@inproceedings{DBLP:journals/entcs/Platzer07,
author = {Andr{\'e} Platzer},
title = {Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems},
booktitle = {Proc., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA},
year = {2007},
editor = {Patrick Blackburn and Thomas Bolander and Torben Bra\"{u}ner and Valeria de Paiva and J{\o}rgen Villadsen},
series = {ENTCS},
journal = {Electr. Notes Theor. Comput. Sci.},
issn = {15710661},
volume = {174},
number = {6},
month = {Jun},
pages = {6377},
doi = {10.1016/j.entcs.2006.11.026},
url = {http://symbolaris.com/pub/hdL.pdf},
keywords = {hybrid logic, dynamic logic, sequent calculus, compositional verification, realtime hybrid dynamic systems},
abstract = { We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces statebased reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goaloriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus. } } 
[inproceedings] bibtexE. R. Olderog and B. Steffen, "Formale Semantik und Programmverifikation," in Proc. InformatikHandbuch, 4. Auflage, 2006, pp. 145166.
@inproceedings{erobs06,
author = {E.R. Olderog and B. Steffen},
title = {{F}ormale {S}emantik und {P}rogrammverifikation},
booktitle = {InformatikHandbuch, 4. Auflage},
editor = {P. Rechenberg and G. Pomberger},
year = 2006, publisher = {Hanser Verlag},
pages = {145166} } 
[inproceedings] bibtexR. Meyer, "Model Checking the $\pi$Calculus," in Proc. Proceedings of the International Research Training Groups Workshop, 2006, p. 15.
@inproceedings{Meyer2006Dagstuhl,
author = {R. Meyer},
title = {Model Checking the $\pi$Calculus},
booktitle = {Proceedings of the International Research Training Groups Workshop},
pages = {15},
year = {2006},
volume = {3},
series = {Trustworthy Software Systems},
publisher = {GITO},
publists = {rmeyer} } 
[inproceedings] bibtexJ. D. Quesel and A. Schäfer, "SpatioTemporal Model Checking for Mobile RealTime Systems," in Proc. 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, 2006, pp. 347361.
@inproceedings{QS06,
author = {J.D. Quesel and A. Sch\"afer},
title = {SpatioTemporal Model Checking for Mobile RealTime Systems},
booktitle = {3rd International Colloquium on Theoretical Aspects of Computing, ICTAC},
year = {2006},
editor = {K. Barkaoui and A. Cavalcanti and A. Cerone},
series = {LNCS},
pages = {347361},
publists = {schaefer,quesel},
abstract = { This paper presents an automatic verification method for combined temporal and spatial properties of mobile realtime systems. To this end, we provide a translation of the Shape Calculus (SC), a spatiotemporal extension of Duration Calculus, into weak second order logic of one successor (WS1S). A prototypical implementation facilitates successful verification of spatiotemporal properties by translating SC specifications into the syntax of the WS1S checker MONA. For demonstrating the formalism and tool usage, we apply it to the benchmark case study ``generalised railroad crossing'' (GRC) enriched by requirements inexpressible in nonspatial formalisms. } } 
[article] bibtexW. Damm, H. Hungar, and E. R. Olderog, "Verification of cooperating traffic agents," International Journal of Control, vol. 79, iss. 5, pp. 395421, 2006.
@article{DHO06,
author = {W. Damm and H. Hungar and E.R. Olderog},
title = {Verification of cooperating traffic agents},
journal = {International Journal of Control},
year = {2006},
optkey = {},
volume = {79},
number = {5},
month = {May},
pages = {395421},
abstract = { This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented verification methodology is equally applicable for avionics applications (such as TCAS, the Traffic Alert and Collision Avoidance System), train applications (such as ETCS, the European Train Control System), or automotive applications (such as platooning). We present a verification rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind ``a collision will never occur'', and whose premises can either be established by offline analysis of the worstcase behavior of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. A companion paper will show how such local proof obligations can be discharged automatically. } } 
[incollection] bibtexR. Meyer, "Model Checking Using Testing," in Dependability Engineering, Hasselbring, W. and Giesecke, S., Eds., GITO, 2006, vol. 2, pp. 147171.
@incollection{Meyer2006,
author = {R. Meyer},
title = {Model Checking Using Testing},
booktitle = {Dependability Engineering},
pages = {147171},
publisher = {GITO},
year = {2006},
editor = {W. Hasselbring and S. Giesecke},
volume = {2},
series = {Trustworthy Software Systems},
publists = {rmeyer} } 
[inproceedings] bibtexJ. Faber and R. Meyer, "Model Checking DataDependent RealTime Properties of the European Train Control System," in Proc. Formal Methods in Computer Aided Design, 2006. FMCAD '06, 2006, pp. 7677.
@inproceedings{FR06,
author = {J. Faber and R. Meyer},
title = {Model Checking DataDependent RealTime Properties of the European Train Control System},
booktitle = {Formal Methods in Computer Aided Design, 2006. FMCAD '06},
year = {2006},
month = nov, pages = {7677},
publisher = {IEEE Computer Society Press},
note = {This publication is available free of charge at \url{http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.21} {IEEE Digital Library}},
publists = {rmeyer},
abstract = { The behavior of embedded hardware and software systems is determined by at least three dimensions: control flow, data aspects, and realtime requirements. To specify the different dimensions of a system with the bestsuited techniques, the formal language CSPOZDC integrates Communicating Sequential Processes (CSP), ObjectZ (OZ), and Duration Calculus (DC) into a declarative formalism equipped with a unified and compositional semantics. In this paper, we provide evidence that CSPOZDC is a convenient language for modeling systems of industrial relevance. To this end, we examine the emergency message handling in the European Train Control System (ETCS) as a case study with uninterpreted constants and infinite data domains. We automatically verify that our model ensures realtime safety properties, which crucially depend on the system?s data handling. } } 
[inproceedings] bibtexT. Strazny and C. Stehno, "Ein Simulator für mehrfach erweiterte höhere Petrinetze," in Proc. 19. Symposium Simulationstechnik (ASIM 2006), 2006, pp. 171176.
@inproceedings{SS06,
author = {Tim Strazny and Christian Stehno},
title = {{E}in {S}imulator {f}\"{u}r {m}ehrfach {e}rweiterte {h}\"{o}here {P}etrinetze},
booktitle = {19. Symposium Simulationstechnik (ASIM 2006)},
editor = {Matthias Becker and Helena Szczerbicka},
year = {2006},
month = sep, pages = {171176},
publisher = {SCS Publishing House e.V.},
publists = {strazny},
abstract = {Petrinetze mit ihrer eindeutigen Semantik und dem zugrunde liegenden mathematischen Modell bew\"{a}hren sich vermehrt bei Entwurf, Analyse und Steuerung komplexer, asynchroner und verteilter Systeme. Insbesondere zeitbehaftete stochastische gef\"{a}rbte Petrinetze bieten M\"{o}glichkeiten komplizierte Sachverhalte strukturiert und kompakt auszudr\"{u}cken, jedoch ist die Simulation solcher h\"{o}heren Petrinetze um ein Vielfaches aufw\"{a}ndiger. Mit Geschwindigkeit und Vielf\"{a}ltigkeit als Hauptziel wurde mit PUMLaut/Sim ein Simulator f\"{u}r solche mehrfach erweiterten Petrinetze entwickelt.} } 
[article] bibtex  Go to documentI. Brückner, B. Metzler, and H. Wehrheim, "Optimizing Slicing of Formal Specifications by Deductive Verification," Nordic Journal of Computing, vol. 13, iss. 12, pp. 2245, 2006.
@article{BMW06,
author = {I. Br\"uckner and B. Metzler and H. Wehrheim},
title = {Optimizing Slicing of Formal Specifications by Deductive Verification},
journal = {Nordic Journal of Computing},
year = {2006},
volume = {13},
number = {12},
month = {August},
pages = {2245},
publists = {brueckner,wehrheim},
abstract = { Slicing is a technique for extracting parts of programs or specifications with respect to certain criteria of interest. The extraction is carried out in such a way that properties as described by the slicing criterion are preserved, i.e., they hold in the complete program if and only if they hold in the sliced program. During verification, slicing is often employed to reduce the state space of specifications to a size tractable by a model checker. The computation of specification slices relies on the construction of dependence graphs, reflecting (at least) control and data dependencies in specifications. The more dependencies the graph has, the less removal of parts is possible. In this paper we present a technique for optimizing the construction of the dependence graph by using deductive verification techniques. More precisely, we propose a technique for showing that certain control dependencies in the graph can be eliminated. The technique employs small {\em deductive} proofs of the enabledness of certain transitions. Thereby we obtain dependence graphs with less control dependencies and as a consequence smaller specification slices which are an easier target for model checking. },
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib06njc.pdf} } 
[inproceedings] bibtexP. E. Sevinç, D. Basin, and E. R. Olderog, "Controlling Access to Documents: A Formal Access Control Model," in Proc. ETRICS 2006, 2006, pp. 352367.
@inproceedings{SBO06,
author = {P. E. Sevin\c{c} and D. Basin and E.R. Olderog},
booktitle = {ETRICS 2006},
editor = {G\"unter M\"uller},
month = {June},
pages = {352367},
publisher = {SpringerVerlag},
series = {LNCS},
title = {Controlling Access to Documents: A Formal Access Control Model},
volume = 3995, year = 2006, abstract = { Current accesscontrol systems for documents suffer from one or more of the following limitations: they are coarsegrained, limited to XML documents, ot unable to maintain control over copies of documents once they are released by the system. We present a formal model of a system that overcomes all of these restrictions. It is very finegrained, supporst a general class of documents, and provides a foundation for usage control. } } 
[inproceedings] bibtexR. Meyer, J. Faber, and A. Rybalchenko, "Model Checking Duration Calculus: A Practical Approach," in Proc. Theoretical Aspects of Computing  ICTAC 2006, 2006, pp. 332346.
@inproceedings{MFR2006,
author = {R. Meyer and J. Faber and A. Rybalchenko},
title = {Model Checking Duration Calculus: A Practical Approach},
booktitle = {Theoretical Aspects of Computing  ICTAC 2006},
year = {2006},
editor = {K. Barkaoui and A. Cavalcanti and A. Cerone},
series = {LNCS},
volume = {4281},
pages = {332346},
pdf = {http://csd.informatik.unioldenburg.de/~jfaber/dl/MeyerFaberRybalchenko2006.pdf},
note = {This publication is available at \url{ http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11921240_23 } {SpringerLink}},
publists = {rmeyer,pea},
abstract = { Model checking of realtime systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automatabased semantics. This task is difficult to automate. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to real world applications. Our algorithm significantly extends the subset of DC that can be handled. It decomposes DC specifications into subproperties that can be verified independently. The decomposition bases on a novel distributive law for DC. We implemented the algorithm as part of our tool chain for the automated verification of systems comprising data, communication, and realtime aspects. Our translation facilitated a successful application of the tool chain on an industrial case study from the European Train Control System (ETCS). } } 
[inproceedings] bibtex  Go to documentB. Beckert and A. Platzer, "Dynamic Logic with Nonrigid Functions: A Basis for Objectoriented Program Verification," in Proc. Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 1720, 2006, Proceedings, 2006, pp. 266280.
@inproceedings{DBLP:conf/cade/BeckertP06,
author = {Bernhard Beckert and Andr{\'e} Platzer},
title = {Dynamic Logic with Nonrigid Functions: A Basis for Objectoriented Program Verification},
booktitle = {Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 1720, 2006, Proceedings},
year = {2006},
editor = {U. Furbach and N. Shankar},
volume = {4130},
series = {LNCS},
subseries = {LNAI},
pages = {266280},
doi = {10.1007/11814771_23},
issn = {03029743},
isbn = {3540371877},
publisher = {SpringerVerlag},
keywords = {dynamic logic, sequent calculus, program logic, software verification, logical foundations of programming languages, objectorientation},
note = {\url{http://dx.doi.org/10.1007/11814771_23}{(c) SpringerVerlag}},
url = {http://symbolaris.com/pub/odl.pdf},
abstract = { We introduce a dynamic logic that is enriched by nonrigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a (relatively) complete sequent calculus for this logic. In conjunction with dynamically typed object enumerators, nonrigid functions allow to embed notions of objectorientation in dynamic logic, thereby forming a basis for verification of objectoriented programs. A semantical generalisation of substitutions, called state update, which we add to the logic, constitutes the central technical device for dealing with object aliasing during function modification. With these few extensions, our dynamic logic captures the essential aspects of the complex verification system KeY and, hence, constitutes a foundation for objectoriented verification with the principles of reasoning that underly the successful KeY case studies. } }
Publications 2000  2005

[inproceedings] bibtexH. Dierks, "Finding Optimal Plans for Domains with Continuous Effects with UPPAAL CORA," in Proc. Proceedings of the ICAPS'05 Workshop on Verification and Validation of ModelBased Planning and Scheduling Systems, 2005.
@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 ModelBased Planning and Scheduling Systems}},
month = {June},
year = {2005} } 
[misc] bibtexI. Brückner, Slicing CSPOZ Specifications for Verification, 2005.
@misc{ib05zb,
author = {I. Br{\"u}ckner},
title = {{Slicing CSPOZ Specifications for Verification}},
howpublished = {Poster Session, 4th International Conference of B and Z Users (ZB '05)},
month = {April},
year = {2005},
publists = {brueckner} } 
[article] bibtexE. R. Olderog and H. Wehrheim, "Specification and (property) inheritance in CSPOZ," Science of Computer Programming, vol. 55, pp. 227257, 2005.
@article{OW05,
author = {E.R. Olderog and H. Wehrheim},
title = {{Specification and (property) inheritance in CSPOZ}},
journal = {Science of Computer Programming},
year = {2005},
volume = {55},
pages = {227257},
abstract = { CSPOZ [Fis97, Fis00] is a combination of Communicating Sequential Processes (CSP) and ObjectZ (OZ). It enables the specification of systems having both a statebased and a behaviouroriented view using the objectoriented concepts of classes, instantiation and inheritance. CSPOZ has a process semantics in the failure divergence model of CSP. In this paper we explain CSPOZ and investigate the notion of inheritance. Furthermore, we study the issue of property inheritance among classes. We prove in a uniform way that behavioural subtyping relations between classes introduced in [Weh02] guarantee the inheritance of safety and ``liveness'' properties. \emph{Key words}: CSP, ObjectZ, failures divergence semantics, inheritance, safety and ``liveness'' properties, modelchecking, FDR \begin{thebibliography} \bibitem{Fis97} C.~Fischer. \newblock {CSPOZ}: A combination of {ObjectZ} and {CSP}. \newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open ObjectBased Distributed Systems (FMOODS'97)},
volume~2, pages 423438. Chapman \& Hall, 1997. \bibitem{Fis00} C.~Fischer. \newblock {\em Combination and Implementation of Processes and Data: From {CSPOZ} to {Java}}. \newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000. \bibitem{Weh02} H.~Wehrheim. \newblock Behavioural subtyping in objectoriented specification formalisms. \newblock University of Oldenburg, Habilitation Thesis, 2002. \end{thebibliography} } } 
[techreport] bibtex  Go to documentI. Brückner and H. Wehrheim, "Slicing ObjectZ Specifications for Verification," SFB/TR 14 AVACS, http://www.avacs.org/, 3, 2005.
@techreport{BW05aTR,
author = {I. Br\"uckner and H. Wehrheim},
title = {{Slicing ObjectZ Specifications for Verification}},
number = {3},
institution = {{SFB/TR 14 AVACS}},
address = {http://www.avacs.org/},
url = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_003.pdf},
year = {2005},
publists = {brueckner,wehrheim} } 
[techreport] bibtex  Go to documentI. Brückner and H. Wehrheim, "Slicing CSPOZ Specifications for Verification," SFB/TR 14 AVACS, http://www.avacs.org/, 7, 2005.
@techreport{BW05bTR,
author = {I. Br\"uckner and H. Wehrheim},
title = {{Slicing CSPOZ Specifications for Verification}},
number = {7},
institution = {{SFB/TR 14 AVACS}},
address = {http://www.avacs.org/},
url = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_007.pdf},
year = {2005},
publists = {brueckner,wehrheim} } 
[inproceedings] bibtexC. Eichner, H. Fleischhack, R. Meyer, U. Schrimpf, and C. Stehno, "Compositional Semantics for UML 2.0 Sequence Diagrams Using Petri Nets," in Proc. SDL 2005: Model Driven, 2005, pp. 133148.
@inproceedings{EichnerFleischhackMeyerSchrimpfStehno2005,
author = {C. Eichner and H. Fleischhack and R. Meyer and U. Schrimpf and C. Stehno},
title = {Compositional Semantics for UML 2.0 Sequence Diagrams Using Petri Nets},
booktitle = {{SDL} 2005: Model Driven},
year = {2005},
pages = {133148},
series = {LNCS},
volume = {3530},
publisher = {SpringerVerlag},
publists = {rmeyer} } 
[inproceedings] bibtex  Go to documentI. Brückner and B. Metzler, "Deductive Verification for Improving Slicing of Integrated Formal Specifications," in Proc. Proceedings of the 17th Nordic Workshop on Programming Theory, 2005, pp. 3941.
@inproceedings{ibnwpt05,
author = {I. Br{\"u}ckner and B. Metzler},
title = {{Deductive Verification for Improving Slicing of Integrated Formal Specifications}},
booktitle = {Proceedings of the 17th Nordic Workshop on Programming Theory},
publisher = {University of Copenhagen, Denmark},
pages = {3941},
year = {2005},
month = {October},
publists = {brueckner},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib05nwpt.pdf} } 
[inproceedings] bibtex  Go to documentM. Möller, "Mapping Formal Specifications to Java Contracts," in Proc. Proceedings of the 17th Nordic Workshop on Programming Theory, 2005, pp. 100102.
@inproceedings{mm05nwpt,
author = {M. M\"oller},
title = {Mapping Formal Specifications to Java Contracts},
booktitle = {Proceedings of the 17th Nordic Workshop on Programming Theory},
publisher = {University of Copenhagen, Denmark},
pages = {100102},
year = {2005},
month = {October},
publists = {moeller,formoos},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/mm05nwpt.pdf} } 
[inproceedings] bibtex  Go to documentJ. Faber, "Verifying RealTime aspects of the European Train Control System," in Proc. Proceedings of the 17th Nordic Workshop on Programming Theory, 2005, pp. 6770.
@inproceedings{nwpt05,
author = {J. Faber},
title = {Verifying RealTime aspects of the {European Train Control System}},
booktitle = {Proceedings of the 17th Nordic Workshop on Programming Theory},
publisher = {University of Copenhagen, Denmark},
pages = {6770},
year = {2005},
month = {October},
publists = {faber},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/jf05nwpt.pdf} } 
[inproceedings] bibtex  Go to documentJ. Hoenicke and P. Maier, "ModelChecking of Specifications Integrating Processes, Data and Time," in Proc. FM 2005, 2005, pp. 465480.
@inproceedings{HoenickeMaierFM2005,
author = {Jochen Hoenicke and Patrick Maier},
title = {ModelChecking of Specifications Integrating Processes, Data and Time},
booktitle = {FM 2005},
editor = {J.S. Fitzgerald and I.J. Hayes and A. Tarlecki},
series = {LNCS},
volume = {3582},
publisher = {Springer},
year = {2005},
pages = {465480},
url = {http://csd.Informatik.UniOldenburg.DE/~skript/pub/Papers/hm05fm.pdf},
publists = {pea},
abstract = { We present a new modelchecking technique for CSPOZDC, a combination of CSP, ObjectZ and Duration Calculus, that allows reasoning about systems exhibiting communication, data and realtime aspects. As intermediate layer we will use a new kind of timed automata that preserve events and data variables of the specification. These automata have a simple operational semantics that is amenable to verification by a constraintbased abstractionrefinement model checker. By means of a case study, a simple elevator parameterised by the number of floors, we show that this approach admits modelchecking parameterised and infinite state realtime systems. } } 
[inproceedings] bibtex  Go to documentR. Boute and A. Schäfer, "The Timer Cascade: Functional Modelling and Real Time Calculi," in Proc. Theoretical Aspects of Computing, ICTAC 2005, 2005, pp. 242256.
@inproceedings{BS05,
author = {R. Boute and A. Sch\"afer},
title = {The Timer Cascade: Functional Modelling and Real Time Calculi},
booktitle = {Theoretical Aspects of Computing, ICTAC 2005},
pages = {242  256},
year = {2005},
editor = {D.V. Hung and M. Wirsing},
volume = {3722},
series = {LNCS},
publisher = {Springer},
url = {http://csd.Informatik.UniOldenburg.DE/~skript/pub/Papers/bs05.pdf},
note = {This publication is available at \url{ http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11560647_16 } {SpringerLink} },
publists = {schaefer},
abstract = { Case studies can significantly contribute towards improving the understanding of formalisms and thereby to their applicability in practice. One such case, namely a cascade of the familiar 24hour timers (in suitably generalized form) provides interesting gedanken experiments and illustrations for presenting, illustrating and comparing various formalisms for modelling realtime behaviour of systems. The timer cascade is first modelled in a generalpurpose functional formalism (Funmath) and various properties are derived, including an interesting algebraic monoid structure of timer programs. Then it is described and analyzed in duration calculus, thereby highlighting, similarities and differences in the approach to modelling and reasoning, and also the link between the formalisms. Future work consists in using this case as a running example for exploring the same issues for other formalisms intended for real time and hybrid systems. The underlying idea is that other authors join this effort and contribute towards extending it, finally arriving at a broad comparative survey of such formalisms. } } 
[inproceedings] bibtex  Go to documentA. Schäfer, "A calculus for shapes in time and space," in Proc. Theoretical Aspects of Computing, ICTAC 2004, 2005, pp. 463478.
@inproceedings{sch05,
author = {A. Sch\"afer},
title = {A calculus for shapes in time and space},
booktitle = {Theoretical Aspects of Computing, ICTAC 2004},
pages = {463478},
year = {2005},
editor = {Z. Liu and K. Araki},
volume = {3407},
series = {LNCS},
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/as05a.pdf},
publisher = {Springer},
note = {This publication is available at \url{ http://springerlink.metapress.com/openurl.asp?genre=article&issn=03029743&volum e=3407&spage=463} {SpringerLink} },
publists = {schaefer},
abstract = { We present a spatial and temporal logic based on Duration Calculus for the specification and verification of mobile realtime systems. We demonstrate the use of the formalism and apply it to a case study. We extend a pure Duration Calculus specification for the controller by spatial assumptions to reason about spatial system properties. We prove that the formalism is undecidable in general for discrete and continuous domains and present a decidable fragment. } } 
[inproceedings] bibtex  Go to documentA. Schäfer, "Axiomatisation and Decidability of MultiDimensional Duration Calculus," in Proc. Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, TIME 2005, 2005, pp. 122130.
@inproceedings{sch05b,
author = {A. Sch\"afer},
title = {{Axiomatisation and Decidability of MultiDimensional Duration Calculus}},
booktitle = {Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, {TIME} 2005},
pages = {122130},
month = {June},
year = {2005},
editor = {J. Chomicki and D. Toman},
volume = {},
series = {},
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/as05.pdf},
publisher = {IEEE Computer Society},
note = {This publication is available at \url{http://doi.ieeecomputersociety.org/10.1109/TIME.2005.15} {IEEE Digital Library} },
publists = {schaefer},
abstract = { We investigate properties of a spatiotemporal logic based on an ndimensional Duration Calculus tailored for the specification and verification of mobile realtime systems. After showing nonaxiomatisability, we give a complete embedding in ndimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use. } } 
[inproceedings] bibtex  Go to documentI. Brückner and H. Wehrheim, "Slicing ObjectZ Specifications for Verification," in Proc. ZB 2005: Formal Specification and Development in Z and B, 2005, pp. 414433.
@inproceedings{BW05a,
author = {I. Br\"uckner and H. Wehrheim},
title = {{Slicing ObjectZ Specifications for Verification}},
booktitle = {ZB 2005: Formal Specification and Development in Z and B},
series = {LNCS},
volume = {3455},
publisher = {Springer},
issn = {03029743},
isbn = {3540255591},
editor = {H. Treharne and S. King and M. Henson and S. Schneider},
pages = {414433},
month = {April},
year = {2005},
publists = {brueckner,wehrheim},
abstract = { Slicing is the activity of reducing a program or a specification with respect to a given condition (the slicing criterion) such that the condition holds on the full program if and only if it holds on the reduced program. Originating from program analysis the entity to be sliced is usually a program and the slicing criterion a value of a variable at a certain program point. In this paper we present an approach to slicing ObjectZ specifications with temporal logic formulae as slicing criteria and show the correctness of our approach. The underlying motivation is the goal to substantially reduce the size of the specification and subsequently facilitate verification of temporal logic properties. },
note = {This publication is available at \url{ http://springerlink.metapress.com/openurl.asp?genre=article&issn=03029743&volum e=3455&spage=414} {SpringerLink} },
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib05zb.pdf} } 
[inproceedings] bibtex  Go to documentI. Brückner and H. Wehrheim, "Slicing an Integrated Formal Method for Verification," in Proc. ICFEM 2005: Seventh International Conference on Formal Engineering Methods, 2005, pp. 360374.
@inproceedings{BW05b,
author = {Ingo Br\"uckner and Heike Wehrheim},
title = {{Slicing an Integrated Formal Method for Verification}},
booktitle = {ICFEM 2005: Seventh International Conference on Formal Engineering Methods},
series = {Lecture Notes in Computer Science},
volume = {3785},
publisher = {Springer},
issn = {03029743},
isbn = {3540297979},
editor = {KungKiu Lau and Richard Banach},
pages = {360374},
month = {November},
year = {2005},
abstract = { Model checking specifications with complex data and behaviour descriptions often fails due to the large state space to be processed. In this paper we propose a technique for {\em reducing} such specifications (with respect to certain properties under interest) before verification. The method is an adaption of the {\em slicing technique} from program analysis to the area of integrated formal notations and temporal logic properties. It solely operates on the syntactic structure of the specification which is usually significantly smaller than its state space. We show how to build a reduced specification via the construction of a so called program dependence graph, and prove correctness of the technique with respect to a projection relationship between full and reduced specification. The reduction thus preserves all properties formulated in temporal logics which are invariant under stuttering, as for instance LTL$_{X}$. },
note = { This publication is available at \url{ http://springerlink.metapress.com/openurl.asp?genre=article&issn=03029743&volum e=3785&spage=360} {SpringerLink} },
publists = {brueckner,wehrheim},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib05icfem.pdf} } 
[incollection] bibtexC. Fischer and H. Wehrheim, "FailureDivergence Semantics as a Formal Basis for an ObjectOriented Integrated Formal Method," in Current Trends in Theoretical Computer Science: The Challenge of the New Century, Vol 2: Formal Models and Semantics, Paun, G., Rozenberg, G., and Salomaa, A., Eds., World Scientific, 2004.
@incollection{FiWe04,
author = {C. Fischer and H. Wehrheim},
editor = {G. Paun and G. Rozenberg and A. Salomaa},
title = {{FailureDivergence Semantics as a Formal Basis for an ObjectOriented Integrated Formal Method}},
publisher = {World Scientific},
year = {2004},
booktitle = {Current Trends in Theoretical Computer Science: The Challenge of the New Century, Vol 2: Formal Models and Semantics} } 
[inproceedings] bibtexH. Wehrheim, "Preserving properties under change," in Proc. FMCO 2003: Formal Methods for Components and Objects, 2004, pp. 330343.
@inproceedings{Weh04,
author = {H. Wehrheim},
title = {Preserving properties under change},
booktitle = {FMCO 2003: Formal Methods for Components and Objects},
year = {2004},
editor = {F.S. de Boer and M.M. Bonsangue and S. Graf and W.P. de Roever},
volume = {3188},
pages = {330343},
series = {LNCS} } 
[inproceedings] bibtexW. Damm, H. Hungar, and E. R. Olderog, "On the Verification of Cooperating Traffic Agents," in Proc. FMCO 2003: Formal Methods for Components and Objects, 2004, pp. 77110.
@inproceedings{DaHuOl04,
author = {W. Damm and H. Hungar and E.R. Olderog},
title = {On the Verification of Cooperating Traffic Agents},
booktitle = {FMCO 2003: Formal Methods for Components and Objects},
year = {2004},
editor = {F.S. de Boer and M.M. Bonsangue and S. Graf and W.P. de Roever},
volume = {3188},
pages = {77110},
series = {LNCS},
abstract = { This paper exploits design patterns employed in coordinating autonomous transport vehicles so as to ease the burden in verifying cooperating hybrid systems. The presented veri cation methodology is equally applicable for avionics applications (such as TCAS), train applications (such as ETCS), or automotive applications (such as platooning). We present a veri cation rule explicating the essence of employed design patters, guaranteeing global safety properties of the kind ``a collision will never occur'', and whose premises can either be established by o line analysis of the worstcase behavior of the involved tra c agents, or by purely local proofs, involving only a single tra c agent. In a companion paper we will show, how such local proof obligations can be discharged automatically. } } 
[inproceedings] bibtex  Go to documentM. Bretschneider, H. J. Holberg, E. Böde, I. Brückner, T. Peikenkamp, and H. Spenke, "Modelbased Safety Analysis of a Flap Control System," in Proc. Proceedings of the 14th Annual International INCOSE Symposium 2004, Toulouse, 2004.
@inproceedings{incose04,
author = {M. Bretschneider and H.J. Holberg and E. B\"ode and I. Br\"uckner and T. Peikenkamp and H. Spenke},
title = {{Modelbased Safety Analysis of a Flap Control System}},
booktitle = {Proceedings of the 14th Annual International INCOSE Symposium 2004, Toulouse},
editor = {T. Fossnes and M. Galinier},
month = {June},
year = {2004},
abstract = { Fault tree analysis is a widely adopted technique to systematically analyze causes for a given failure of a complex system. Traditionally, a fault tree is constructed topdown based on knowledge about the structure of the system and the interaction of subsystems. With the increasing system complexity and the accompanying introduction of modelbased development techniques in the industrial process, a substantial amount of this knowledge is laid down in the system models. The main focus of the presented techniques and tools is to automatically exploit this knowledge by extracting a fault tree suitable for FaulTree+ directly from a given design modeled in Statemate. The resulting fault tree is complete wrt. the specified failure, i.e. the analysis considers every possible causal failure combination which is guaranteed by applying model checking techniques. Using an aircraft Flap control system this paper shows how to smoothly integrate the technique into an existing modelbased process. },
publists = {brueckner},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib04ft.pdf} } 
[inproceedings] bibtexH. Dierks, "Heuristic Guided ModelChecking of RealTime Systems," in Proc. Proceedings of the 16th Nordic Workshop on Programming Theory, 2004, pp. 1416.
@inproceedings{Die04b,
author = {H. Dierks},
title = {Heuristic Guided ModelChecking of RealTime Systems},
editor = {P. Pettersson and Wang Yi},
booktitle = {{Proceedings of the 16th Nordic Workshop on Programming Theory}},
pages = {1416},
series = {Technical Reports of the Department of Information Technology},
number = {2004041},
publisher = {Uppsala University, Sweden},
issn = {14043203},
year = {2004},
month = {October} } 
[inproceedings] bibtex  Go to documentI. Brückner, "Slicing CSPOZ Specifications," in Proc. Proceedings of the 16th Nordic Workshop on Programming Theory, 2004, pp. 7173.
@inproceedings{nwpt04,
author = {I. Br{\"u}ckner},
title = {{Slicing CSPOZ Specifications}},
editor = {P. Pettersson and W. Yi},
booktitle = {Proceedings of the 16th Nordic Workshop on Programming Theory},
series = {Technical Reports of the Department of Information Technology},
number = {2004041},
publisher = {Uppsala University, Sweden},
issn = {14043203},
pages = {7173},
year = {2004},
month = {October},
publists = {brueckner},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib04nwpt.pdf} } 
[article] bibtex  Go to documentR. Buschermöhle, M. Brörkens, I. Brückner, W. Damm, W. Hasselbring, B. Josko, C. Schulte, and T. Wolf, "Model Checking  Grundlagen und Praxiserfahrungen," Informatik Spektrum, vol. 27, iss. 2, pp. 146158, 2004.
@article{mcp04,
author = {R. Buscherm\"ohle and M. Br\"orkens and I. Br\"uckner and W. Damm and W. Hasselbring and B. Josko and C. Schulte and T. Wolf},
title = {{Model Checking  Grundlagen und Praxiserfahrungen}},
journal = {Informatik Spektrum},
editor = {A. Bode},
issn = {01706012},
publisher = {Springer Verlag},
volume = {27},
number = {2},
pages = {146158},
month = {April},
year = {2004},
abstract = { The correct functioning of hard and software components is often a crucial factor in computerbased system engineering. Particularly, this is the case in the area of 'safety critical' systems, where a system failure can endanger human life. But also in less critical areas the correctness of provided functionality becomes more and more important. Furthermore the complexity of system functionality increases steadily. Therefore manual test and simulation methods can detect many errors only with inaccaptable high effort concerning time and resources. Starting from this background, this article presents the basics of 'model checking', an automatic and complete verification method. Based on this introduction, experience gained with the application of model checking tools in industrial contexts is presented and discussed. },
publists = {brueckner},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib04mc.pdf} } 
[inproceedings] bibtex  Go to documentM. Möller, E. R. Olderog, H. Rasch, and H. Wehrheim, "Linking CSPOZ with UML and Java: A Case Study," in Proc. Integrated Formal Methods, 2004, pp. 267286.
@inproceedings{MORW04,
author = {M. M\"oller and E.R. Olderog and H. Rasch and H. Wehrheim},
title = {{Linking CSPOZ with UML and Java: A Case Study}},
editor = {E. Boiten and J. Derrick and G. Smith},
booktitle = {Integrated Formal Methods},
series = {Lecture Notes in Computer Science},
number = {2999},
publisher = springer, issn = {03029743},
pages = {267286},
year = {2004},
month = {March},
abstract = { We describe how CSPOZ, an integrated formal method combining the process algebra CSP with the specification language ObjectZ, can be linked to standard software engineering languages, viz.\ UML and Java. Our aim is to generate a significant part of the CSPOZ specification from an initially developed UML model using a UML profile for CSPOZ, and afterwards transform the formal specification into assertions written in the Java Modelling Language JML complemented by CSP$_{jassda}$. The intermediate CSPOZ specification serves to verify correctness of the UML model, and the assertions control at runtime the adherence of a Java implementation to these formal requirements. We explain this approach using the case study of a ``holonic manufacturing system'' in which coordination of transportation and processing is distributed among stores, machine tools and agents without central control. },
url = {http://csd.informatik.unioldenburg.de/pub/Papers/morw04.pdf},
publists = {moeller formoos} } 
[article] bibtexH. Wehrheim, "Behavioral Subtyping Relations for Active Objects," Formal Methods in System Design, vol. 23, iss. 2, pp. 143170, 2003.
@article{Weh03b,
author = {H. Wehrheim},
title = {{Behavioral Subtyping Relations for Active Objects}},
journal = {Formal Methods in System Design},
volume = {23},
number = {2},
pages = {143170},
year = {2003} } 
[inproceedings] bibtex  Go to documentJ. Derrick and H. Wehrheim, "Using coupled simulations in nonatomic refinement," in Proc. ZB 2003: Formal Specification and Development in Z and B, 2003, pp. 127147.
@inproceedings{DeWe03, title = {Using coupled simulations in nonatomic refinement},
author = {J. Derrick and H. Wehrheim},
editor = {D. Bert and J. Bowen and S. King and M. Walden},
booktitle = {ZB 2003: Formal Specification and Development in Z and B},
volume = {2651},
series = {LNCS},
pages = {127147},
publisher = {Springer},
url = {http://csd.informatik.unioldenburg.de/~wehrheim/ZB2003.ps},
year = {2003} } 
[inproceedings] bibtexE. R. Olderog and H. Wehrheim, "Specification and Inheritance in CSPOZ," in Proc. Formal Methods for Components and Objects, 2003, pp. 361379.
@inproceedings{OlWe02,
author = {E.R. Olderog and H. Wehrheim},
title = {{Specification and Inheritance in CSPOZ}},
editor = {F. de Boer and M. Bosangue and S. Graf and W.P. de Roever},
booktitle = {Formal Methods for Components and Objects},
volume = {2852},
series = {LNCS},
pages = {361379},
publisher = {Springer},
year = {2003},
abstract = { CSPOZ [Fis97,Fis00] is a combination of Communicating Sequential Processes (CSP) and ObjectZ (OZ). It enables the specification of systems having both a statebased and a behaviouroriented view using the objectoriented concepts of classes, instantiation and inheritance. CSPOZ has a process semantics in the failures divergence model of CSP. In this paper we explain CSPOZ and investigate the notion of inheritance. Behavioural subtyping relations between classes introduced in [Weh02] guarantee the inheritance of safety and ``liveness'' properties. \begin{thebibliography} \bibitem{Fis97} C.~Fischer. \newblock {CSPOZ}: A combination of {ObjectZ} and {CSP}. \newblock In H.~Bowman and J.~Derrick, editors, {\em Formal Methods for Open ObjectBased Distributed Systems (FMOODS'97)},
volume~2, pages 423438. Chapman \& Hall, 1997. \bibitem{Fis00} C.~Fischer. \newblock {\em Combination and Implementation of Processes and Data: From {CSPOZ} to {Java}}. \newblock PhD thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000. \bibitem{Weh02} H.~Wehrheim. \newblock Behavioural subtyping in objectoriented specification formalisms. \newblock University of Oldenburg, Habilitation Thesis, 2002. \end{thebibliography} } } 
[inproceedings] bibtex  Go to documentH. Wehrheim, "Inheritance of Temporal Logic Properties," in Proc. Formal Methods for Open Objectbased Distributed Systems, 2003, pp. 7993.
@inproceedings{We03,
author = {H. Wehrheim},
title = {{Inheritance of Temporal Logic Properties}},
editor = {E. Najm and U. Nestmann and P. Stevens},
booktitle = {Formal Methods for Open Objectbased Distributed Systems},
volume = {2884},
series = {LNCS},
pages = {7993},
publisher = {Springer},
url = {http://csd.informatik.unioldenburg.de/~wehrheim/Fmoods03.ps},
year = {2003} } 
[article] bibtexE. R. Olderog and H. Dierks, "Moby/RT: A Tool for Specification and Verification of RealTime Systems," Journal of Universal Computer Science, vol. 9, pp. 88105, 2003.
@article{OD03,
author = {E.R. Olderog and H. Dierks},
title = {{Moby/RT: A Tool for Specification and Verification of RealTime Systems}},
journal = {Journal of Universal Computer Science},
year = {2003},
optkey = {},
volume = {9},
optnumber = {},
pages = {88105},
optmonth = {},
optnote = {},
abstract = { The tool Moby/RT supports the design of realtime systems at the levels of requirements, design specifications and programs. Requirements are expressed by constraint diagrams [Kle00], design specifications by PLCAutomata [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 MobyRT by discussing its semantic basis and its use for automatic verification by utilising the modelchecker 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 {PLCAutomata: A New Class of Implementable RealTime Automata}. \newblock {\em TCS},
253(1):6193. \end{thebibliography} } } 
[article] bibtex  Go to documentC. Schulte, M. Brörkens, I. Brückner, R. Buschermöhle, and T. Wolf, "Sicherheit für sicherheitskritische Systeme," Electronic Embedded Systeme, pp. 1921, 2003.
@article{mcpees03,
author = {C. Schulte and M. Br\"orkens and I. Br\"uckner and R. Buscherm\"ohle and T. Wolf},
title = {{Sicherheit f\"ur sicherheitskritische Systeme}},
journal = {Electronic Embedded Systeme},
issn = {09434941},
publisher = {AWi Verlag},
month = {September},
pages = {1921},
year = {2003},
abstract = { Mikroprozessoren werden immer h\"aufiger auch in technischen Ger\"aten und vielerlei allt\"aglichen Konsumg\"utern eingesetzt. Letzere werden auch als eingebettete Systeme bezeichnet, das hei\ss{}t in umgebende technische Systeme wechselseitig integrierte Computersysteme. Die Entwicklung solcher eingebetteter Systeme wird unter anderem aufgrund immer h\"oherer Anforderungen an die Funktionalit\"at und einer wachsenden Anzahl von interagierenden Komponenten immer komplexer. Um diesem Umstand Rechnung zu tragen, werden in Prozessmodellen und Standards, die insbesondere im Bereich sicherheitskritischer Systeme angewendet werden, bereits seit geraumer Zeit vollst\"andige Korrektheitsnachweise gefordert. Ein aussichtsreicher Kandidat in diesem Kontext ist das ModelChecking. },
publists = {brueckner},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ib03.pdf} } 
[inproceedings] bibtex  Go to documentH. Dierks and J. Tapken, "\sc Moby/DC  A Tool for ModelChecking Parametric RealTime Specifications," in Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), 2003, pp. 271277.
@inproceedings{DT03,
author = {H. Dierks and J. Tapken},
title = {{\sc Moby/DC}  {A} Tool for ModelChecking Parametric RealTime Specifications},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003)},
editor = {H. Garavel and J. Hatcliff},
year = {2003},
pages = {271277},
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 realtime system descriptions that contain timing parameters. We introduce the tool Moby/DC which implements a modelchecking algorithm for phase automata. The algorithm applies compositional modelchecking techniques and handles parameters by builtin procedures or by a link to CLP(R). Due to the parameters the modelchecking 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 modelchecker especially well suited for proving the absence of error traces instead of finding them. },
url = {http://csd.informatik.unioldenburg.de/~dierks/Berichte/TACAS03.ps.gz} } 
[inproceedings] bibtex  Go to documentH. Rasch and H. Wehrheim, "Checking Consistency in UML Diagrams: Classes and State Machines," in Proc. Formal Methods for Open Objectbased Distributed Systems, 2003, pp. 229243.
@inproceedings{RaWe03,
author = {H. Rasch and H. Wehrheim},
title = {{Checking Consistency in UML Diagrams: Classes and State Machines}},
editor = {E. Najm and U. Nestmann and P. Stevens},
booktitle = {Formal Methods for Open Objectbased Distributed Systems},
volume = {2884},
series = {LNCS},
pages = {229243},
publisher = {Springer},
year = {2003},
url = {http://csd.informatik.unioldenburg.de/~wehrheim/RaWe03.ps},
publists = {formoos} } 
[article] bibtexH. Dierks and E. R. Olderog, "Temporale Spezifikationslogiken," atAutomatisierungstechnik, vol. 51, iss. 2, p. a1a4, 2003.
@article{DO03,
author = {H. Dierks and E.R. Olderog},
title = {{Temporale Spezifikationslogiken}},
journal = {atAutomatisierungstechnik},
year = {2003},
optkey = {},
volume = {51},
number = {2},
optmonth = {},
pages = {A1A4},
optnote = {},
optannote = {},
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] bibtex  Go to documentA. Schäfer, "Combining RealTime ModelChecking and Fault Tree Analysis," in Proc. FM 2003: the 12th International FME Symposium, 2003, pp. 522541.
@inproceedings{sch03,
author = {A. Sch\"afer},
title = {Combining RealTime ModelChecking and Fault Tree Analysis},
booktitle = {FM 2003: the 12th International FME Symposium },
year = {2003},
editor = {D. Mandrioli and K. Araki and S. Gnesi},
volume = {2805},
series = {LNCS},
pages = {522541},
publisher = {Springer},
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/as03.pdf},
note = {This publication is available at \url{ http://www.springerlink.com/openurl.asp?genre=article&issn=03029743&volume=2805 &spage=522} {SpringerLink} },
publists = {schaefer},
abstract = { We present a semantics for fault tree analysis, a technique used for the analysis of safety critical systems, in the realtime interval logic Duration Calculus with Liveness and show how properties of fault trees can be checked automatically. We apply this technique in two examples and show how it can be connected to other verification techniques. } } 
[article] bibtexJ. Hoenicke and E. R. Olderog, "CSPOZDC: A Combination of Specification Techniques for Processes, Data and Time," Nordic Journal of Computing, vol. 9, iss. 4, pp. 301334, 2002.
@article{HO02b,
author = {J. Hoenicke and E.R. Olderog},
title = {{CSPOZDC}: A Combination of Specification Techniques for Processes, Data and Time},
journal = {Nordic Journal of Computing},
year = {2002},
volume = {9},
number = {4},
pages = {301334},
note = {appeared March 2003},
abstract = { CSPOZDC is a new combination of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], ObjectZ [Smi00], and Duration Calculus [ZHR91]. This combination is illustrated by specifying the train controller of a case study on radio controlled railway crossings. The technical contribution of the paper is a smooth integration of the underlying semantic models and its use for verifying timing properties of CSPOZDC specifications. This is done by combining the modelcheckers FDR [Ros94] for CSP and UPPAAL [BLL97] for timed automata with a new tool \emph{f2u} that transforms FDR transition systems and certain patterns of Duration Calculus formulae into timed automata. This approach is illustrated by the example of a vending machine. \begin{thebibliography} \bibitem{BLL97} J.~Bengtsson, K.G. Larsen, F.~Larsson, P.~Pettersson, and Wang Yi. \newblock Uppaal  a tool suite for automatic verification of realtime systems. \newblock In R.~Alur, T.A. Henzinger, and E.D. Sonntag, editors, {\em Hybrid Systems III  Verification and Control},
volume 1066 of {\em LNCS},
pages 232243. Springer, 1997. \bibitem{Hoa85} C.A.R. Hoare. \newblock {\em Communicating Sequential Processes}. \newblock Prentice Hall, 1985. \bibitem{Ros94} A.W. Roscoe. \newblock Modelchecking {CSP}. \newblock In A.W. Roscoe, editor, {\em A Classical Mind  Essays in Honour of C.A.R.Hoare},
pages 353378. PrenticeHall, 1994. \bibitem{Smi00} G.~Smith. \newblock {\em The ObjectZ Specification Language}. \newblock Kluwer Academic Publisher, 2000. \bibitem{ZHR91} C.~Zhou, C.A.R. Hoare, and A.P. Ravn. \newblock A calculus of durations. \newblock {\em Information Processing Letters},
40(5):269276, 1991. \end{thebibliography} } } 
[article] bibtexH. Wehrheim, "Relating Statebased and Behaviouroriented Subtyping," Nordic Journal of Computing, vol. 9, iss. 4, pp. 405435, 2002.
@article{weh03,
author = {H. Wehrheim},
title = {Relating Statebased and Behaviouroriented Subtyping},
journal = {Nordic Journal of Computing},
year = {2002},
volume = {9},
number = {4},
pages = {405435},
note = {appeared March 2003},
abstract = { Subtyping relations for objectoriented formalisms describe relationships between classes which satisfy the substitutability requirement imposed on types and their subtypes. Subtyping relations have been proposed both for statebased and for behaviouroriented specification formalisms. In this paper we state and proof correspondence results between these two forms of subtyping: starting from a statebased specification language we show that via a behaviouroriented semantics statebased subtyping induces behaviouroriented subtyping. In the comparison we study three different kinds of subtyping achieving substitutivity to a different degree. For all three kinds of definitions a correspondence result can be shown. } } 
[inproceedings] bibtex  Go to documentH. Wehrheim, "Checking Behavioural Subtypes via Refinement," in Proc. FMOODS 2002: Formal Methods for Open ObjectBased Distributed Systems, 2002, pp. 7993.
@inproceedings{weh02,
author = {H. Wehrheim},
title = {Checking Behavioural Subtypes via Refinement},
booktitle = {FMOODS 2002: Formal Methods for Open ObjectBased Distributed Systems},
editor = {B. Jacobs and A. Rensink},
year = {2002},
month = {May},
pages = {7993},
publisher = {Kluwer},
publists = {formoos},
abstract = { Behavioural subtyping is concerned with the question of whether one class is behaviourally consistent with another class. The word ``behaviour'' in this context usually refers to the semantics of methods, typically given by pre and postconditions. In this paper, we will use this term in a more specific way, referring to the dynamic behaviour of objects in time. Behaviour descriptions of classes give sequencing constraints on method invocations, in this paper formulated using the process algebra CSP. Behavioural subtyping can be seen as a mixture of refinement and inheritance: we expect the subtype to be substitutable for the supertype while at the same moment allowing extension of functionality. Since refinement itself does not allow extension of functionality, a subtyping definition must therefore extend standard refinement concepts to cope with additional methods in the subtype. In this paper, we show for three such subtyping relations how they can, despite these extensions, be checked via refinement. This gives us the possibility of employing standard refinement checkers for CSP (viz. the FDR modelchecker) for subtype checks. },
url = {http://csd.informatik.unioldenburg.de/~wehrheim/fmoods02.ps} } 
[inproceedings] bibtex  Go to documentJ. Hoenicke and E. R. Olderog, "Combining Specification Techniques for Processes Data and Time," in Proc. Integrated Formal Methods, 2002, pp. 245266.
@inproceedings{ho02,
author = {J. Hoenicke and E.R. Olderog},
title = {{Combining Specification Techniques for Processes Data and Time}},
editor = {M. Butler and L. Petre and K. Sere},
booktitle = {Integrated Formal Methods},
series = {Lecture Notes in Computer Science},
volume = {2335},
publisher = springer, url = {http://csd.Informatik.UniOldenburg.DE/~skript/pub/Papers/ho02ifm.pdf},
year = {2002},
month = {May},
pages = {245266},
abstract = { We present a new combination CSPOZDC of three well researched formal techniques for the specification of processes, data and time: CSP [Hoa85], ObjectZ [Smi00], and Duration Calculus [ZHR91]. The emphasis is on a smooth integration of the underlying semantic models and its use for verifying properties of CSPOZDC specifications by a combined application of the modelcheckers FDR [Ros94] for CSP and UPPAAL [BLL97] for Timed Automata. This approach is applied to part of a case study on radio controlled railway crossings. } } 
[inproceedings] bibtex  Go to documentM. Brörkens and M. Möller, "Dynamic Event Generation for Runtime Checking using the JDI," in Proc. Proceedings of the Second Workshop on Runtime Verification (RV'02), Copenhagen, Denmark, July 2002, 2002.
@inproceedings{mbmm02b,
author = {M. Br\"orkens and M. M\"oller},
title = {{Dynamic Event Generation for Runtime Checking using the JDI}},
booktitle = {Proceedings of the Second Workshop on Runtime Verification (RV'02), Copenhagen, Denmark, July 2002},
publisher = {Elsevier Science},
editor = {Klaus Havelund and Grigore Rosu},
volume = 70, number = 4, series = {Electronic Notes in Theoretical Computer Science},
year = 2002, month = {July},
note = {This publication is available at \url{http://www.elsevier.nl/locate/entcs/volume70.html}{ENTCS}},
publists = {moeller formoos},
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/jassdaevents.pdf},
abstract = { Approaches to runtime checking have to track the execution of a software system and therefore have to deal with generating and processing execution events. Often these techniques are applied at the code level  either by inserting new source code prior to the compilation or by modifying the target code, e.g. Java byte code, before running the program. The \textsf{jassda} framework and tool enable runtime checking of Java programs against a CSPlike specification. For generating events it uses the Java Debug Interface (JDI) and thus no modifications to the code are necessary. Another advantage is that events are generated on demand, i.e. dynamically at runtime it is determined which events to generate for the current debug run without modifying the program itself. This paper shows how this event generation is done by the \textsf{jassda} framework. } } 
[inproceedings] bibtex  Go to documentH. Dierks, G. Behrmann, and K. G. Larsen, "Solving Planning Problems Using RealTime ModelChecking (Translating PDDL3 into Timed Automata)," in Proc. AIPSWorkshop Planning via ModelChecking, 2002, pp. 3039.
@inproceedings{DBL02,
author = {H. Dierks and G. Behrmann and K.G. Larsen},
title = {{Solving Planning Problems Using RealTime ModelChecking (Translating PDDL3 into Timed Automata)}},
booktitle = {{AIPSWorkshop Planning via ModelChecking}},
optcrossref = {},
optkey = {},
pages = {3039},
year = {2002},
editor = {F. Kabanza and S. Thiebaux},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = apr, optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://csd.Informatik.UniOldenburg.DE/~dierks/Berichte/AIPS.ps.gz} } 
[inproceedings] bibtex  Go to documentH. Dierks and M. Lettrari, "Constructing Test Automata from Graphical RealTime Requirements," in Proc. FTRTFT 2002, 2002, pp. 433453.
@inproceedings{DL02,
author = {H. Dierks and M. Lettrari},
title = {{Constructing Test Automata from Graphical RealTime Requirements}},
booktitle = {FTRTFT 2002},
optcrossref = {LNCS2469},
optkey = {},
pages = {433453},
year = {2002},
opteditor = {},
optvolume = {},
optnumber = {},
series = lncs, optaddress = {},
month = sep, optorganization = {},
publisher = springer, optnote = {},
optannote = {},
url = {http://csd.Informatik.UniOldenburg.DE/~dierks/Berichte/FTRTFT02.ps.gz} } 
[inproceedings] bibtexH. Rasch and H. Wehrheim, "Consistency between UML Classes and Associated State Machines," in Proc. UML 2002  Workshop on Consistency Problems in UMLbased Software Development, 2002, pp. 4660.
@inproceedings{rawe02,
author = {H. Rasch and H. Wehrheim},
title = {Consistency between {UML} Classes and Associated State Machines},
optcrossref = {},
optkey = {},
booktitle = {{UML} 2002  Workshop on Consistency Problems in {UML}based Software Development},
pages = {4660},
year = {2002},
editor = {L. Kuzniarz and G. Reggio and J. L. Sourrouille and Z. Huzar},
volume = {06},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
publists = {formoos} } 
[inproceedings] bibtex  Go to documentM. Brörkens and M. Möller, "jassda Trace Assertions," in Proc. Trends in Testing Communicating Systems, Berlin, Germany, 2002, pp. 3948.
@inproceedings{mbmm02,
author = {M. Br\"orkens and M. M\"oller},
title = {{jassda Trace Assertions}},
booktitle = {Trends in Testing Communicating Systems},
optcrossref = {},
optkey = {},
pages = {3948},
year = {2002},
editor = {Ina Schieferdecker and Hartmut K\"onig and Adam Wolisz},
optvolume = {},
optnumber = {},
series = {International Confernece on Testing Communicating Systems (TestCom)},
address = {Berlin, Germany},
month = {March},
optorganization = {Frauenhofer Gesellschaft},
optpublisher = {},
optnote = {to be published as Technical Report by Frauenhofer Gesellschaft},
optannote = {},
publists = {moeller},
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/mbmm02.pdf} } 
[inproceedings] bibtex  Go to documentM. Möller, "Specifying and Checking Java using CSP," in Proc. Workshop on Formal Techniques for Javalike Programs  FTfJP'2002, 2002.
@inproceedings{mm02,
author = {Michael M\"oller},
title = {{Specifying and Checking Java using CSP}},
booktitle = {Workshop on Formal Techniques for Javalike Programs  FTfJP'2002},
optcrossref = {},
optkey = {},
optpages = {},
year = {2002},
opteditor = {},
optvolume = {},
optnumber = {Technical Report NIIIR0204},
optseries = {},
optaddress = {},
month = {June},
organization = {Computing Science Department, University of Nijmegen},
optpublisher = {},
note = {Technical Report NIIIR0204},
optannote = {},
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/csp4j.pdf},
publists = {moeller formoos},
abstract = { Currently several approaches are done in applying formal techniques to the Java programming language. A new trend is to take dynamic behaviour into account when designing such techniques. To bring formal techniques to practical applications one often has to reduce the goal coming down from full verification to runtime checking. \textsf{jassda} is a framework for performing such runtime checks at the bytecode level of Java. The TraceChecker module of \textsf{jassda} allows one to test the dynamic behaviour of multiple Java virtual machines by monitoring whether the trace of all relevant events is a member of the trace semantics of a given CSP process or not. In this paper we present the CSP dialect that is used to specify a set of allowed traces for Java programs. The underlying semantics allows partial specifications of distributed Java programs and to recombine them while preserving properties. } } 
[article] bibtexA. Rensink and H. Wehrheim, "Process algebra with action dependencies," Acta Informatica, iss. 38, pp. 155234, 2001.
@article{rewe01,
author = {A. Rensink and H. Wehrheim},
title = {Process algebra with action dependencies},
journal = {Acta Informatica},
number = {38},
pages = {155234},
year = {2001} } 
[misc] bibtex  Go to documentJ. Hoenicke, Specification of Radio Based Railway Crossings with the Combination of CSP, OZ, and DC, 2001.
@misc{hoe01,
author = {J. Hoenicke},
title = {{Specification of Radio Based Railway Crossings with the Combination of CSP, OZ, and DC}},
month = jun, year = 2001, howpublished = {FBT 2001},
url = {http://www.iu.de/fbt2001/fbt2001_docs/hoenicke.ps} } 
[inproceedings] bibtex  Go to documentH. Wehrheim, "Patterns and Rules for Behavioural Subtyping," in Proc. FORTE 2001, 2001, pp. 335352.
@inproceedings{weh01,
author = {Heike Wehrheim},
title = {{Patterns and Rules for Behavioural Subtyping}},
booktitle = {FORTE 2001},
editor = {M. Kim and B. Chin and S. Kang and D. Lee},
pages = {335  352},
publisher = {Kluwer},
abstract = { Subtyping relations for objectoriented formalisms describe relationships between super and subclasses which satisfy the substitutability requirement imposed on types and their subtypes. Behavioural subtyping is concerned with subtypes for active classes with an explicit dynamic behaviour, specifiable for instance by objectoriented formal methods combining statebased with behavioural formalisms. Such specification languages often have a formal semantics that composes behavioural semantics for both the behaviour and the statebased part. In this paper we develop syntactic patterns and semantic rules for the statebased part of a subclass which guarantee that the subclass is a behavioural subtype of its superclass. This allows to check for subtypes without computing the behavioural semantics of the class at all. Our results are similar to the ones linking data refinement in statebased methods with failuredivergence refinement in CSP. In contrast to classical data refinement, subtyping (and the simulation relations used for showing the soundness of the patterns) have to cope with additional new operations in the subclass. },
url = {http://csd.informatik.unioldenburg.de/~wehrheim/forte01.ps},
year = {2001} } 
[article] bibtexH. Dierks and J. Tapken, "Moby/PLC: Eine graphische Entwicklungsumgebung für SPSProgramme," atAutomatisierungstechnik, vol. 1, pp. 3844, 2001.
@article{dt01,
author = {H. Dierks and J. Tapken},
title = {{Moby/PLC: Eine graphische Entwicklungsumgebung f{\"u}r SPSProgramme}},
journal = {atAutomatisierungstechnik},
year = {2001},
optkey = {},
volume = {1},
optnumber = {},
optmonth = {},
pages = {3844},
optnote = {},
optannote = {},
publists = {MobyPLC} } 
[inproceedings] bibtex  Go to documentD. Bartetzko, C. Fischer, M. Möller, and H. Wehrheim, "Jass  Java with Assertions," in Proc. Proceedings of the First Workshop on Runtime Verification (RV'01), Paris, France, July 2001, 2001.
@inproceedings{bfmw01,
author = {D. Bartetzko and C. Fischer and M. M\"oller and H. Wehrheim},
title = {{Jass  Java with Assertions}},
booktitle = {Proceedings of the First Workshop on Runtime Verification (RV'01), Paris, France, July 2001},
publisher = {Elsevier Science},
editor = {Klaus Havelund and Grigore Rosu},
volume = 55, number = 2, series = {Electronic Notes in Theoretical Computer Science},
year = 2001, note = {This publication is available at \url{http://www.elsevier.nl/locate/entcs/volume55.html} {ENTCS} },
publists = {moeller formoos},
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/jass.pdf},
abstract = { Design by Contract, proposed by Meyer for the programming language Eiffel, is a technique that allows runtime checks of specification violation and their treatment during program execution. \jass, {\bf J}ava with {\bf ass}ertions, is a Design by Contract extension for Java allowing to annotate Java programs with specifications in the form of assertions. The \jass{} tool is a precompiler that translates annotated into pure Java programs in which compliance with the specification is dynamically tested. Besides the standard Design by Contract features known from classical program verification (e.g. pre and postconditions, invariants), \jass{} additionally supports \emph{refinement},
i.e. subtyping, \emph{checks} and the novel concept of \emph{trace assertions}. Trace assertions are used to monitor the dynamic behaviour of objects in time. } } 
[inproceedings] bibtexM. Broy and E. R. Olderog, "TraceOriented Models of Concurrency," in Proc. Handbook of Process Algebra, 2001, pp. 101195.
@inproceedings{bo01,
author = {M. Broy and E.R. Olderog},
title = {{TraceOriented Models of Concurrency}},
booktitle = {Handbook of Process Algebra},
optcrossref = {},
optkey = {},
pages = {101195},
year = {2001},
editor = {J.A. Bergstra and A. Ponse and S.A. Scott},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
publisher = {Elsevier Science B.V.},
optnote = {},
abstract = { This chapter provides an indepth presentation of traceoriented models of concurrent processes. We begin by introducing and investigating finite traces as a simple abstraction of the transition behaviour of automata. Using finite traces safety properties of processes can be modelled. Later infinite traces or {\it streams} together with stream processing functions are studied. Using infinite traces more advanced phenomena like fairness and liveness properties can be modelled. We discuss and relate operational, denotational, algebraic and logical approaches to traceoriented models and explain methods for the specification and verification of process behaviour based on these models. } } 
[inproceedings] bibtex  Go to documentC. Fischer, E. R. Olderog, and H. Wehrheim, "A CSP view on UMLRT structure diagrams," in Proc. Fundamental Approaches to Software Engineering, 2001, pp. 91108.
@inproceedings{fow01,
author = {C. Fischer and E.R. Olderog and H. Wehrheim},
title = {{A CSP view on UMLRT structure diagrams}},
booktitle = {{Fundamental Approaches to Software Engineering}},
optcrossref = {},
optkey = {},
pages = {91108},
year = {2001},
editor = {H. Husmann},
volume = {2029},
optnumber = {},
series = lncs, optaddress = {},
optmonth = {},
optorganization = {},
publisher = springer, optnote = {},
optannote = {},
abstract = { UMLRT is an extension of UML for modelling embedded reactive and realtime software systems. Its particular focus lies on system descriptions on the architectural level, defining the overall system structure. In this paper we propose to use UMLRT structure diagrams together with the formal method CSPOZ combining CSP and ObjectZ. While CSPOZ is used for specifying the system components themselves (by CSPOZ classes), UMLRT diagrams provide the architecture description. Thus the usual architecture specification in terms of the CSP operators parallel composition, renaming and hiding is replaced by a graphical description. To preserve the formal semantics of CSPOZ specifications, we develop a translation from UMLRT structure diagrams to CSP. Besides achieving a more easily accessible, graphical architecture modelling for CSPOZ, we thus also give a semantics to UMLRT structure diagrams. },
publists = {formoos},
url = {http://csd.informatik.unioldenburg.de/~wehrheim/fase01.ps} } 
[article] bibtexH. Wehrheim, "Data Abstraction Techniques in the Validation of CSPOZ Specifications," Formal Aspects of Computing, vol. 12, 2000.
@article{weh00d,
author = {H. Wehrheim},
title = {{Data Abstraction Techniques in the Validation of CSPOZ Specifications}},
journal = {Formal Aspects of Computing},
year = {2000},
volume = {12},
page = {147164} } 
[inproceedings] bibtexH. Wehrheim, "Subtyping patterns for active objects," in Proc. Proceedings 8ter Workshop des GIArbeitskreises GROOM: Visuelle Verhaltensmodellierung verteilter und nebenläufiger SoftwareSysteme, 2000.
@inproceedings{weh00c,
author = {Heike Wehrheim},
title = {Subtyping patterns for active objects},
editor = {H. Giese and S. Philippi},
booktitle = {Proceedings 8ter Workshop des GIArbeitskreises GROOM: Visuelle Verhaltensmodellierung verteilter und nebenl\"aufiger SoftwareSysteme},
publisher = {Universit\"at M\"unster},
note = {No. 24/00I},
year = {2000} } 
[article] bibtex  Go to documentC. Fischer and H. Wehrheim, "FailureDivergence Semantics as a Formal Basis for an ObjectOriented Integrated Formal Method," Bulletin of the EATCS (European Association of Theoretical Computer Science), vol. 71, pp. 92101, 2000.
@article{fiwe00b,
author = {Clemens Fischer and Heike Wehrheim},
title = {FailureDivergence Semantics as a Formal Basis for an ObjectOriented Integrated Formal Method},
journal = {Bulletin of the EATCS (European Association of Theoretical Computer Science)},
volume = {71},
pages = {92  101},
url = {http://csd.informatik.unioldenburg.de/~wehrheim/Eatcs.ps},
abstract = { The integration of several different modelling techniques into a single formal method has turned out to be advantageous in the formal design of software systems. Giving a semantics to an integrated formal method is currently a very active area of research. In this paper we discuss the advantages of a failuredivergence semantics for data and process integrating formal methods, in particular for those with a concept of inheritance. The discussion proceeds along the lines of the formal method CSPOZ, a combination of CSP and ObjectZ, developed in Oldenburg. },
year = {2000} } 
[inproceedings] bibtex  Go to documentH. Wehrheim, "Behavioural Subtyping and Property Preservation," in Proc. FMOODS'00: Formal Methods for Open ObjectBased Distributed Systems, 2000.
@inproceedings{weh00b,
author = {Heike Wehrheim},
title = {Behavioural Subtyping and Property Preservation},
booktitle = {FMOODS'00: Formal Methods for Open ObjectBased Distributed Systems},
editor = {S. Smith and C. Talcott},
publisher = {Kluwer},
abstract = { Inheritance is one of the key features in objectoriented design and analysis. It especially supports an incremental development by allowing to stepwise add new functionality to an existing system design. When using a subclass which is a specialisation of a certain superclass, the question arises which of the superclass' properties still hold for the subclass. We investigate this topic for three behavioural subtyping relations, which formalise the subtype  supertype relationship among classes on the basis of process algebra correctness relations. According to the degree of change allowed by the subtyping relations, safety and liveness properties of the superclass are preserved up to different extents. },
url = {http://csd.informatik.unioldenburg.de/~wehrheim/fmoods00.ps},
year = {2000} } 
[inproceedings] bibtexJ. Bredereke, "Families of Formal Requirements in Telephone Switching," in Proc. Feature Interactions in Telecommunications and Software Systems VI, Amsterdam, 2000.
@inproceedings{bre:fiw00,
author = {Jan Bredereke},
title = {Families of Formal Requirements in Telephone Switching},
booktitle = {Feature Interactions in Telecommunications and Software Systems {VI}},
publisher = {{IOS Press}},
year = {2000},
month = {May},
address = {Amsterdam},
note = {Submitted. An abstract is available {\url{http://csd.informatik.unioldenburg.de/~jan/abstracts/Bre99e.html} {here}}},
publists = {} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and A. P. Ravn, "Documenting Design Refinement," in Proc. Proc. of the Third Workshop on Formal Methods in Software Practice, 2000, pp. 89100.
@inproceedings{or00,
author = {E.R. Olderog and A.P. Ravn},
title = {Documenting Design Refinement},
editor = {M.P.E. Heimdahl},
booktitle = {Proc. of the Third Workshop on Formal Methods in Software Practice},
pages = {89100},
publisher = {ACM},
year = {2000},
abstract = { We show how UML class diagrams can be used to document design by refinement in the early design stages. This is illustrated by an example from the area of embedded realtime and hybrid systems. A precise semantics is given for the UML class diagrams by translation to the Z schema calculus. },
url = {http://csd.Informatik.UniOldenburg.DE/pub/Papers/or00.ps} } 
[article] bibtexH. Dierks, "PLCAutomata: A New Class of Implementable RealTime Automata ," tcs, vol. 253, iss. 1, pp. 6193, 2000.
@article{die00,
author = {H. Dierks},
title = {{PLCAutomata: A New Class of Implementable RealTime Automata }},
journal = tcs, year = {2000},
optkey = {},
volume = {253},
number = {1},
month = dec, pages = {6193},
note = {full version of \cite{hd97arts}},
optannote = {} } 
[inproceedings] bibtex  Go to documentH. Wehrheim, "Specification of an Automatic Manufacturing System  A case study in using integrated formal methods," in Proc. FASE 2000, Fundamental Approaches to Software Engineering, 2000.
@inproceedings{weh2000,
author = {Heike Wehrheim},
title = {Specification of an Automatic Manufacturing System  A case study in using integrated formal methods},
editor = {},
booktitle = {FASE 2000, Fundamental Approaches to Software Engineering},
series = {LNCS},
volume = {1783},
publists = {cspoz formoos},
note = {},
abstract = { An automatic manufacturing system serves as a case study for the applicability of an integrated formal method to the specification of software systems. The formal method chosen is CSPOZ, an integration of the stateoriented formalism ObjectZ with the process algebra CSP. The practicability as well as limitations of CSPOZ are studied. We furthermore employ a graphical notation (class diagrams) from the Unified Modelling Language to describe the architectural view of the system. The correctness of the obtained specification is checked by a translation into the input language of the CSP model checker FDR and a following property check. },
url = {http://csd.informatik.unioldenburg.de/~wehrheim/fase00.ps},
year = {2000} } 
[article] bibtex  Go to documentH. Dierks and J. Tapken, "Modelling and Verifying of `CashPoint Service' Using Moby/PLC," Formal Aspects of Computing, vol. 12, pp. 222221, 2000.
@article{dt00,
author = {H. Dierks and J. Tapken},
title = {{Modelling and Verifying of `CashPoint Service' Using Moby/PLC}},
journal = {Formal Aspects of Computing},
year = {2000},
optkey = {},
volume = {12},
optnumber = {},
optmonth = {},
pages = {222221},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hdjt00.ps.gz},
optannote = {},
publists = {MobyPLC} } 
[inproceedings] bibtex  Go to documentC. Fischer and H. Wehrheim, "Behavioural Subtyping Relations for ObjectOriented Formalisms," in Proc. Algebraic Methodology and Software Technology, 2000, pp. 469483.
@inproceedings{cfhw2000,
author = {Clemens Fischer and Heike Wehrheim},
title = {{Behavioural Subtyping Relations for ObjectOriented Formalisms}},
editor = {T. Rus},
booktitle = {{Algebraic Methodology and Software Technology}},
series = {LNCS},
volume = {1816},
publists = {},
publisher = {Springer},
pages = {469483},
note = {},
abstract = { In this paper we investigate the objectoriented notion of subtyping in the context of behavioural formalisms. Subtyping in OOformalisms is closely related to the concept of inheritance. The central issue in the choice of subtyping relations among classes is the principle of substitutability: an instance of the subtype should be usable wherever an instance of the supertype was expected. Depending on the interpretation of ``usable'', we obtain a variety of subtyping relations: stronger subtyping relations, allowing one to share the subtype instance among different clients without any change compared with the supertype, and weaker relations, restricting the possibilities of interference of different clients on the subtype instance. The subtyping relations are taxonomically ordered in a hierarchy. The concept of ``usability'' is formalised via testing scenarios, which provide alternative characterisations for the subtyping relations. },
url = {http://csd.informatik.unioldenburg.de/~wehrheim/amast00.ps},
year = {2000} } 
[inproceedings] bibtexH. Dierks, "A Process Algebra for RealTime Programs," in Proc. FASE 2000: Fundamental Approaches to Software Engineering, 2000, pp. 6681.
@inproceedings{die00b,
author = {H. Dierks},
title = {{A Process Algebra for RealTime Programs}},
booktitle = {FASE 2000: Fundamental Approaches to Software Engineering},
optcrossref = {LNCS1783},
optkey = {},
editor = {T. Maibaum},
volume = {1783},
optnumber = {},
series = lncs, year = {2000},
optorganization = {},
publisher = springer, optaddress = {},
optmonth = {},
pages = {6681},
optnote = {},
optannote = {} } 
[inproceedings] bibtex  Go to documentH. Dierks, "Specification and Verification of Polling RealTime Systems," in Proc. Ausgezeichnete Informatikdissertationen 1999, 2000.
@inproceedings{die00c,
author = {H. Dierks},
title = {{Specification and Verification of Polling RealTime Systems}},
booktitle = {{Ausgezeichnete Informatikdissertationen 1999}},
optcrossref = {},
optkey = {},
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},
optvolume = {},
optnumber = {},
optseries = {},
year = {2000},
optorganization = {},
publisher = {Teubner},
optaddress = {},
optmonth = {},
optpages = {},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hd00.ps.gz},
optannote = {} }
Publications to 1999

[article] bibtexJ. Bredereke, "Modular, Changeable Requirements in Functional Documentation for Telephone Switching," Formal Methods in System Design, 1999.
@article{bre:changetabtelsys,
author = {Jan Bredereke},
title = {Modular, Changeable Requirements in Functional Documentation for Telephone Switching},
journal = {Formal Methods in System Design},
year = {1999},
note = {Special issue on Tabular Notation. Submitted. An extended abstract is available {\url{http://csd.Informatik.UniOldenburg.DE/~jan/abstracts/Bre99c.html}{here}}} } 
[article] bibtexJ. Bredereke, "Maintaining Telephone Switching Software Requirements," IEEE Communications Magazine, 1999.
@article{bre:ieeecommagmainttelsoft,
author = {Jan Bredereke},
title = {Maintaining Telephone Switching Software Requirements},
journal = {IEEE Communications Magazine},
year = {1999},
note = {Submitted. An abstract is available {\url{http://csd.Informatik.UniOldenburg.DE/~jan/abstracts/Bre99b.html} {here}}} } 
[article] bibtexM. Schenke, "Transformational design of realtime systems  Part 2: from program specifications to programs.," Acta Informatica 36, pp. 6799, 1999.
@article{ms99,
author = {Michael Schenke},
title = {Transformational design of realtime systems  Part 2: from program specifications to programs.},
journal = {Acta Informatica 36},
pages = {6799},
year = {1999} } 
[inproceedings] bibtexJ. Bredereke, "Maintaining Telephone Switching System Requirements," in Proc. Participants' notes of Dagstuhl seminar 99071  software engineering research and education: seeking a new agenda, 1999.
@inproceedings{bre:dagstuhlseagenda,
author = {Jan Bredereke},
title = {Maintaining Telephone Switching System Requirements},
booktitle = {Participants' notes of {Dagstuhl} seminar 99071  software engineering research and education: seeking a new agenda},
year = {1999},
month = {1519~Feb.} } 
[inproceedings] bibtexM. Schenke and A. Lavrov, "Automatabased stochastic analysis of modular hybrid controllers," in Proc. Conference on Probabilistic Analysis of Rare Events (RARE), 1999.
@inproceedings{schla99,
author = {M. Schenke and A. Lavrov},
title = {Automatabased stochastic analysis of modular hybrid controllers},
booktitle = {Conference on Probabilistic Analysis of Rare Events (RARE)},
note = {ISBN 9984668088},
year = {1999} } 
[article] bibtexE.R.Olderog, "Sichere Bahnsteuerungen," Log IN, iss. 1, pp. 6465, 1999.
@article{ero99login,
author = {E.R.Olderog},
title = {Sichere {B}ahnsteuerungen},
journal = {Log {IN}},
pages = {6465},
number = {1},
year = {1999} } 
[article] bibtex  Go to documentM. Schenke and E. R. Olderog, "Transformational design of realtime systems  Part 1: from requirements to program specifications.," Acta Informatica 36, pp. 165, 1999.
@article{msero99,
author = {Michael Schenke and E.R. Olderog},
title = {Transformational design of realtime systems  Part 1: from requirements to program specifications.},
journal = {Acta Informatica 36},
pages = {165},
year = {1999},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/msero97_1.ps.gz} } 
[inproceedings] bibtexM. Schenke and M. Dossis, "Provably Correct Hardware Compilation using Timing Diagrams," in Proc. FORTE/PSTV'99, 1999, pp. 313331.
@inproceedings{schd99, title = {Provably Correct Hardware Compilation using Timing Diagrams},
author = {M. Schenke and M. Dossis},
booktitle = {FORTE/PSTV'99},
publisher = {Kluwer},
pages = {313331},
year = {1999} } 
[inproceedings] bibtexE. R. Olderog, "Correct RealTime Software for Programmable Logic Controllers," in Proc. Correct System Design  Recent Insights and Advances, 1999, pp. 342362.
@inproceedings{ero99,
author = {E.R. Olderog},
title = {{Correct RealTime Software for Programmable Logic Controllers}},
booktitle = {{Correct System Design  Recent Insights and Advances}},
series = {Lecture Notes in Computer Science},
volume = {1710},
publisher = {Springer},
year = {1999},
pages = {342362} } 
[inproceedings] bibtexE. R. Olderog, "Entwicklung korrekter zeitkritischer Systeme," in Proc. Formale Beschreibungstechniken für verteilte Systeme, 1999, pp. 716.
@inproceedings{ero99gi/itg,
author = {E.R. Olderog},
title = {Entwicklung korrekter zeitkritischer {Systeme}},
booktitle = {{Formale} {Beschreibungstechniken} f\"ur verteilte {Systeme}},
editor = {K. Spies and B. Sch\"atz },
series = {GI/ITG Fachgespr\"ach},
volume = {9},
publisher = {Utz Verlag},
year = {1999},
pages = {716} } 
[inproceedings] bibtexB. KriegBrückner, J. Peleska, E. R. Olderog, and A. Baer, "The UniForM Workbench, a Universal Development Environment for Formal Methods," in Proc. FM'99  Formal Methods, 1999, pp. 11861205.
@inproceedings{uniform99,
author = {B. KriegBr\"uckner and J. Peleska and E.R. Olderog and A. Baer},
title = {{The UniForM Workbench, a Universal Development Environment for Formal Methods}},
editor = {J.M. Wing and J. Woodcock and J. Davies},
booktitle = {{FM'99  Formal Methods}},
series = {Lecture Notes in Computer Science},
volume = {1709},
publisher = {Springer},
year = {1999},
pages = {11861205} } 
[techreport] bibtex  Go to documentJ. Bredereke, "Modular, Changeable Requirements for Telephone Switching in CSPOZ," University of Oldenburg, Oldenburg, Germany, Interner Bericht IBS991, 1999.
@techreport{bre:changereqcspoztechrep,
author = {Jan Bredereke},
title = {Modular, Changeable Requirements for Telephone Switching in {CSPOZ}},
institution = {{University of Oldenburg}},
year = {1999},
type = {{Interner Bericht}},
number = {IBS991},
address = {Oldenburg, Germany},
month = {Oct.},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ibs991.ps.gz} } 
[inproceedings] bibtexJ. Bredereke, K. Frühauf, R. Khedri, S. Krauß, and A. Zeller, "Maintenance," in Proc. Software Engineering Research and Education: Seeking a new Agenda, 1999, pp. 4143.
@inproceedings{bre:dagstuhlsemaintenancenoproc,
author = {Jan Bredereke and Karol Fr{\"u}hauf and Ridha Khedri and Stefan Krau{\ss} and Andreas Zeller},
title = {Maintenance},
pages = {4143},
booktitle = {Software Engineering Research and Education: Seeking a new Agenda},
year = {1999},
month = {Feb.},
editor = {Ernst Denert and Daniel Hoffman and Jochen Ludewig and David Parnas},
number = {230},
key = {Dagstuhl},
series = {DagstuhlSeminarReport, ISSN 09401121} } 
[inproceedings] bibtexJ. Atlee, W. Bartussek, J. Bredereke, M. Glinz, R. Khedri, L. Prechelt, and D. Weiss, "Requirements," in Proc. Software Engineering Research and Education: Seeking a new Agenda, 1999, pp. 916.
@inproceedings{bre:dagstuhlserequirementsnoproc,
author = {Joanne Atlee and Wolfram Bartussek and Jan Bredereke and Martin Glinz and Ridha Khedri and Lutz Prechelt and David Weiss},
title = {Requirements},
pages = {916},
booktitle = {Software Engineering Research and Education: Seeking a new Agenda},
year = {1999},
month = {Feb.},
editor = {Ernst Denert and Daniel Hoffman and Jochen Ludewig and David Parnas},
number = {230},
key = {Dagstuhl},
series = {DagstuhlSeminarReport, ISSN 09401121} } 
[inproceedings] bibtex  Go to documentC. Fischer and H. Wehrheim, "ModelChecking CSPOZ Specifications with FDR," in Proc. Proceedings of the 1st International Conference on Integrated Formal Methods (IFM), 1999, pp. 315334.
@inproceedings{cfhw99,
author = {Clemens Fischer and Heike Wehrheim},
title = {ModelChecking {CSPOZ} Specifications with {FDR}},
booktitle = {Proceedings of the 1st International Conference on Integrated Formal Methods (IFM)},
editor = {K. Araki and A. Galloway and K. Taguchi},
year = 1999, pages = {315334},
publisher = {Springer},
publists = {cspoz},
abstract = { CSPOZ is a formal method integrating two different specifications formalisms into one: the formalism ObjectZ for the description of static aspects, and the process algebra CSP for the description of the dynamic behaviour of systems. The semantics of CSPOZ is \emph{failure divergence} taken from the process algebra side. In this paper we propose a method for checking correctness of CSPOZ specifications via a translation into the CSP dialect of the model checker FDR. },
url = {http://csd.informatik.unioldenburg.de/pub/Papers/cfhw99.ps.gz} } 
[article] bibtex  Go to documentH. Dierks, "Synthesizing Controllers from RealTime Specifications," IEEE Transactions on ComputerAided Design of Integrated Circu its and Systems, vol. 18, iss. 1, pp. 3343, 1999.
@article{die99,
author = {H. Dierks},
title = {{Synthesizing Controllers from RealTime Specifications}},
journal = {IEEE Transactions on ComputerAided Design of Integrated Circu its and Systems},
year = {1999},
optkey = {},
volume = {18},
number = {1},
optmonth = {},
pages = {3343},
optnote = {},
url = {http://csd.Informatik.UniOldenburg.DE/~dierks/Berichte/TCAD.ps.gz} } 
[inproceedings] bibtex  Go to documentC. Fischer, "Software Development with ObjectZ, CSP and Java: A Pragmatic Link from Formal Specifications to Programs," in Proc. Formal Techniques for Java Programs, 1999, pp. 2935.
@inproceedings{fischer99:softwdevelobjeczcspjava,
author = {Clemens Fischer},
title = {Software Development with {ObjectZ},
{CSP} and {Java}: A Pragmatic Link from Formal Specifications to Programs},
booktitle = {Formal Techniques for Java Programs},
editor = {B. Jacobs and B. Leavens and P. M\"uller and A. PoetzschHeffter},
volume = 251, series = {Technical Report},
year = 1999, publisher = {Fernuniversit{\"a}t Hagen},
pages = {2935},
publists = {cspoz},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/cspoz2jass.ps.gz} } 
[inproceedings] bibtexJ. Tapken, "Implementing Hierarchical GraphStructures," in Proc. Proceedings of FASE'99, 1999, pp. 219233.
@inproceedings{jt99,
author = {Josef Tapken},
title = {{Implementing Hierarchical GraphStructures}},
booktitle = {Proceedings of FASE'99},
editor = {J.P. Finance},
volume = {1577},
series = {LNCS},
publisher = {SpringerVerlag},
year = {1999},
pages = {219233},
publists = {Mobybg},
note = {\copyright SpringerVerlag. This publication is available {\url{http://csd.informatik.unioldenburg.de/pub/Papers/jt99.ps.gz}{here}} and at {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}} } 
[inproceedings] bibtexE. R. Olderog, "Formal Methods in RealTime Systems," in Proc. Proceedings of the 10th EuroMicro Workshop on Real Time Systems, 1998, pp. 254263.
@inproceedings{ero98:formalmethodrealtimesystem,
author = {E.R. Olderog},
title = {Formal Methods in RealTime Systems},
booktitle = {Proceedings of the 10th EuroMicro Workshop on Real Time Systems},
year = 1998, organization = {IEEE Computer Society},
month = {June},
pages = {254263} } 
[inproceedings] bibtexV. Grabowski, C. Dietz, and E. R. Olderog, "Semantics for Timed Message Sequence Charts via Constraint Diagrams," in Proc. Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC, 1998, pp. 251260.
@inproceedings{erocd98,
author = {V. Grabowski and C. Dietz and E.R. Olderog},
title = {{Semantics for Timed Message Sequence Charts via Constraint Diagrams}},
booktitle = {Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC},
editor = {Y. Lahav and A. Wolisz and J. Fischer and E. Holz},
series = {InformatikBericht Nr. 104},
year = {1998},
pages = {251260},
publisher = {HumboldUniversitaet zu Berlin/Germany} } 
[inproceedings] bibtex  Go to documentH. Dierks and J. Tapken, "ToolSupported Hierarchical Design of Distributed RealTime Systems," in Proc. Euromicro Workshop on Real Time Systems, 1998, pp. 222229.
@inproceedings{hdjt98,
author = {H. Dierks and J. Tapken},
title = {{ToolSupported Hierarchical Design of Distributed RealTime Systems}},
booktitle = {Euromicro Workshop on Real Time Systems},
publisher = {IEEE},
year = {1998},
pages = {222229},
publists = {MobyPLC,Mobybg},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hdjt98.ps.gz} } 
[inproceedings] bibtexS. Kleuker, "Reengineering of Distributed Systems using Formal Methods," in Proc. Proceedings of the Second Euromicro Conference on Software Maintenance and Reengineering, 1998, pp. 189192.
@inproceedings{sk98,
author = {S. Kleuker},
title = {Reengineering of Distributed Systems using Formal Methods},
booktitle = {Proceedings of the Second Euromicro Conference on Software Maintenance and Reengineering},
editor = {P. Nesi and F. Lehner},
publisher = {IEEE Computer Society},
year = 1998, pages = {189192},
publists = {skleuker} } 
[inproceedings] bibtex  Go to documentJ. Bredereke, "Specification Style and Efficiency in Estelle," in Proc. Proc. of the 1st Int'l. Workshop on the Formal Description Technique Estelle  Estelle'98, Evry, France, 1998, pp. 165186.
@inproceedings{bre:estelle98,
author = {Jan Bredereke},
title = {Specification Style and Efficiency in {E}stelle},
pages = {165186},
booktitle = {Proc. of the 1st Int'l. Workshop on the Formal Description Technique {E}stelle  {E}stelle'98},
year = {1998},
editor = {Stanislaw Budkowski and Stefan Fischer and Reinhard Gotzhein},
address = {Evry, France},
month = {2~Nov.},
organization = {Institut National des T{\'e}l{\'e}communications},
url = {http://csd.Informatik.UniOldenburg.DE/~jan/papers/Bre98b.ps.gz} } 
[inproceedings] bibtexJ. Tapken, "Moby/PLC  A Design Tool for Hierarchical RealTime Automata," in Proc. Proceedings of FASE'98, 1998, pp. 326329.
@inproceedings{jt98,
author = {J. Tapken},
title = {{Moby/PLC  A Design Tool for Hierarchical RealTime Automata}},
booktitle = {Proceedings of FASE'98},
editor = {E. Astesiano},
volume = {1382},
series = {LNCS},
publisher = {Springer Verlag},
year = {1998},
pages = {326329},
publists = {MobyPLC} } 
[inproceedings] bibtexC. Fischer, "How to combine Z with a Process Algebra," in Proc. ZUM'98 The Z Formal Specification Notation, 1998, pp. 523.
@inproceedings{fischer98:howzprocesalgeb,
author = {Clemens Fischer},
title = {How to combine {Z} with a Process Algebra},
booktitle = {{ZUM'98} The {Z} Formal Specification Notation},
editor = {J. Bowen and A. Fett and M. Hinchey},
volume = {1493 },
pages = {523},
series = {LNCS},
year = 1998, publisher = {Springer},
publists = {cspoz},
abstract = { The specification language Z has been designed to describe data and functional aspects of systems, but it does not define a semantics for specifications in a distributed setting. Process algebras, on the other hand, concentrate on the behaviour of communicating agents. For this reason the combination of Z with a process algebra recently got a lot of attention. In this paper we summarise and categorise the different approaches and identify pitfalls and shortcomings in existing combinations. Thereby we give an overview over the many possible answers to the question: `What is the behavioural semantics of a Z specification?' } } 
[inproceedings] bibtexC. Fischer and D. Meemken, "JaWA: Java with Assertions," in Proc. JavaInformationsTage, 1998, pp. 4959.
@inproceedings{fischer98:jawa,
author = {Clemens Fischer and D. Meemken},
title = {{JaWA}: {Java} with Assertions},
booktitle = {JavaInformationsTage},
editor = {C. H. Cap},
series = {Informatik aktuell},
year = 1998, publisher = {Springer},
pages = {4959},
note = {In german.},
longauthor = {Clemens Fischer and Dieter Meemken},
abstract = { Methoden zur Entwicklung von korrekter Software und deren Einf\"uhrung in die Praxis stellen heute immer noch ein schwieriges Problem dar. Bertrand Meyer hat unter dem Stichwort 'Programmieren mit Vertrag' einen Vorschlag gemacht und durch Eiffel implementiert, wie man formale Spezifikationsanteile mit Programmcode mischen und zur Laufzeit \"uberpr\"ufen kann. In diesem Paper geben wir einen \"Uberblick \"uber die Sprache JaWA, mit der dieses Konzept auf Java \"ubertragen wurde. JaWA Programme bestehen aus herk\"ommlichem JavaCode, der Zusicherungen (Invarianten, Vor und Nachbedingungen) in Form von Kommentaren enth\"alt. Der JaWAPr\"acompiler \"ubersetzt JaWA in Java. Er erzeugt zus\"atzliche Bedingungen, mit denen die spezifizierten Eigenschaften zur Laufzeit \"uberpr\"uft werden k\"onnen. Dabei wird die Java Ausnahmebehandlung ausgenutzt und um Eiffel \"ahnliche `rescue' und `retry' Anweisungen erg\"anzt. Die erzeugten Fehlermeldungen und Warnungen sind frei konfigurierbar. } } 
[inproceedings] bibtexJ. Tapken and H. Dierks, "Moby/PLC  Graphical Development of PLCAutomata," in Proc. Proceedings of FTRTFT'98, 1998, pp. 311314.
@inproceedings{jthd98,
author = {J. Tapken and H. Dierks},
title = {{Moby/PLC  Graphical Development of PLCAutomata}},
booktitle = {Proceedings of FTRTFT'98},
editor = {A.P. Ravn and H. Rischel},
volume = {1486},
series = {LNCS},
publisher = {Springer Verlag},
year = {1998},
pages = {311314},
note = {\copyright SpringerVerlag. This publication is available {\url{http://csd.informatik.unioldenburg.de/pub/Papers/jthd98.ps.gz}{here}} and at {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}},
publists = {MobyPLC} } 
[proceedings] bibtexFormal Techniques in RealTime and FaultTolerant SystemsLyngby, Denmark: springer, 1998.
@proceedings{all98, title = {{Formal Techniques in RealTime and FaultTolerant Systems}},
year = {1998},
optkey = {},
editor = {A.P. Ravn and H. Rischel},
volume = {1486},
optnumber = {},
series = lncs, publisher = springer, optorganization = {},
address = {Lyngby, Denmark},
month = sep } 
[techreport] bibtex  Go to documentJ. Bredereke, "Requirements Specification and Design of a Simplified Telephone Network by Functional Documentation," McMaster University, Hamilton, Ontario, Canada, CRL Report 367, 1998.
@techreport{bre:studypotsfuncdoc,
author = {Jan Bredereke},
title = {Requirements Specification and Design of a Simplified Telephone Network by Functional Documentation},
institution = {McMaster University},
year = {1998},
type = {CRL Report},
number = {367},
address = {Hamilton, Ontario, Canada},
month = {Dec.},
pages = {86},
issn = {03819337},
url = {http://csd.Informatik.UniOldenburg.DE/~jan/papers/Bre98c.ps.gz} } 
[techreport] bibtex  Go to documentH. Dierks, A. Fehnker, A. Mader, and F. W. Vaandrager, "Operational and Logical Semantics for Polling RealTime Systems," Computer Science Institue Nijmegen, Faculty of Mathematics and Informatics, Catholic University of Nijmegen, CSIR9813, 1998.
@techreport{hd98b,
author = {H. Dierks and A. Fehnker and A. Mader and F.W. Vaandrager},
title = {{Operational and Logical Semantics for Polling RealTime Systems}},
institution = {Computer Science Institue Nijmegen, Faculty of Mathematics and Informatics, Catholic University of Nijmegen},
year = {1998},
optkey = {},
opttype = {},
number = {CSIR9813},
optaddress = {},
publists = {Mobybg},
month = apr, note = {full paper of \cite{hd98c}.},
url = {http://www.cs.kun.nl/csi/reports/info/CSIR9813.html} } 
[inproceedings] bibtexH. Dierks and M. Schenke, "A Unifying Framework for Correct Program Construction," in Proc. Mathematics of Program Construction 98, 1998, pp. 122150.
@inproceedings{hdms98,
author = {H. Dierks and M. Schenke},
title = {{A Unifying Framework for Correct Program Construction}},
booktitle = {Mathematics of Program Construction 98},
optkey = {},
editor = {J. Jeuring},
volume = {1422},
optnumber = {},
series = lncs, year = {1998},
optorganization = {},
publisher = springer, optaddress = {},
month = jun, pages = {122150},
note = {\copyright SpringerVerlag. This publication is available {\url{http://csd.informatik.unioldenburg.de/pub/Papers/MPC.ps.gz}{here}} and at {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}} } 
[inproceedings] bibtexE. R. Olderog and H. Dierks, "Decomposing RealTime Specifications," in Proc. Compositionality: The Significant Difference, 1998, pp. 465489.
@inproceedings{erohd98,
author = {E.R. Olderog and H. Dierks},
title = {{Decomposing RealTime Specifications}},
booktitle = {{Compositionality: The Significant Difference}},
optcrossref = {},
optkey = {},
editor = {H. Langmaack and A. Pnueli and W.P. de Roever},
volume = {1536},
optnumber = {},
series = lncs, year = {1998},
optorganization = {},
publisher = springer, optaddress = {},
optmonth = {},
pages = {465489},
optannote = {},
note = {{\url{http://csd.informatik.unioldenburg.de/pub/Papers/erohd97.ps.gz} {An abstract is available online}}} } 
[inproceedings] bibtex  Go to documentH. Dierks, "Comparing ModelChecking and Logical Reasoning for RealTime Systems," in Proc. ESSLLI'98, 1998.
@inproceedings{hd98a,
author = {H. Dierks},
title = {{Comparing ModelChecking and Logical Reasoning for RealTime Systems}},
booktitle = {ESSLLI'98},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1998},
optorganization = {},
optpublisher = {},
optaddress = {},
publists = {Mobybg},
month = aug, optpages = {},
note = {Workshop proceedings},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ESSLLI.ps.gz} } 
[inproceedings] bibtexH. Dierks, A. Fehnker, A. Mader, and F. W. Vaandrager, "Operational and Logical Semantics for Polling RealTime Systems," in Proc. FTRTFT'98, 1998, pp. 2940.
@inproceedings{hd98c,
author = {H. Dierks and A. Fehnker and A. Mader and F.W. Vaandrager},
title = {{Operational and Logical Semantics for Polling RealTime Systems}},
booktitle = {FTRTFT'98},
optcrossref = {LNCS1486},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
series = lncs, year = {1998},
optorganization = {},
publisher = springer, optaddress = {},
optmonth = {},
pages = {2940},
optnote = {},
publists = {Mobybg},
note = {\copyright SpringerVerlag. This publication is available {\url{http://csd.Informatik.UniOldenburg.DE/~dierks/Berichte/FTRTFT98.ps.gz}{ here}} and at {\url{http://www.springer.de/comp/lncs/index.html}{Springer}}} } 
[misc] bibtexM. Schenke and M. Dossis, Provably Correct Hardware Compilation using Timing Diagrams, 1997.
@misc{msmd97,
author = {Michael Schenke and Michael Dossis},
title = {Provably Correct Hardware Compilation using Timing Diagrams},
note = {Submitted. This publication is available online in two parts. \url{http://csd.informatik.unioldenburg.de/pub/Papers/msmd97p1.ps.gz}{Part 1},
\url{http://csd.informatik.unioldenburg.de/pub/Papers/msmd97p2.ps.gz}{Part 2}.},
year = {1997} } 
[unpublished] bibtex  Go to documentMichael Schenke, Development of Correct RealTime Systems by Refinement, 1997.
@unpublished{ms97habil,
author = {Michael Schenke},
title = {Development of Correct RealTime Systems by Refinement},
note = {Habilitationsschrift.},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ms97habil.ps.gz},
year = {1997} } 
[book] bibtexK. R. Apt and E. R. Olderog, Verification of Sequential and Concurrent Programs., 2nd ed., springer, 1997.
@book{ero97verification,
author = {K.R. Apt and E.R. Olderog},
title = {Verification of Sequential and Concurrent Programs.},
edition = {2nd},
publisher = springer, year = 1997, note = {ISBN 0387948961. \url{http://www.springerny.com/catalog/np/mar97np/DATA/0387948961.html} {This book in the Springer catalogue}. \url{ http://csd.informatik.unioldenburg.de/pub/Papers/ero97verificationa.ps.gz} {More Information}. } } 
[article] bibtexC. Fischer, S. Kleuker, and E. R. Olderog, "Beweisbar korrekte Telekommunikationssysteme," Informationstechnik und Technische Informatik, vol. 3, pp. 2228, 1997.
@article{cfskero97,
author = {C. Fischer and S. Kleuker and E.R. Olderog},
title = {{B}eweisbar korrekte {T}elekommunikationssysteme},
journal = {Informationstechnik und Technische Informatik},
year = 1997, volume = 3, pages = {2228},
note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/cfskero97a.ps.gz} {An extended abstract is available online}},
publists = {skleuker} } 
[inproceedings] bibtex  Go to documentJ. Tapken, "Interactive and Compilative Simulation of PLCAutomata," in Proc. Simulation in Industry, ESS'97, 1997, pp. 552556.
@inproceedings{jt97ess,
author = {Josef Tapken},
title = {{Interactive and Compilative Simulation of PLCAutomata}},
booktitle = {Simulation in Industry, ESS'97},
editor = {Winfried Hahn and Axel Lehmann},
publisher = {Society for Computer Simulation},
year = 1997, pages = {552556},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/jt97ess.ps.gz} } 
[inproceedings] bibtexC. Fischer and G. Smith, "Combining CSP and ObjectZ: Finite or Infinite TraceSemantics?," in Proc. Proceedings of FORTE/PSTV'97, 1997, pp. 503518.
@inproceedings{cfgs97,
author = {Clemens Fischer and Graeme Smith},
title = {Combining {CSP} and {ObjectZ}: Finite or Infinite TraceSemantics?},
booktitle = {Proceedings of FORTE/PSTV'97},
publisher = {Chapmann \& Hall},
editor = {T. Mizuno and N. Shiratori and T. Higashino and A. Togashi},
pages = {503  518},
publists = {cspoz},
note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/cfgs97a.ps} {An abstract is available online}},
year = 1997 } 
[inproceedings] bibtex  Go to documentH. Dierks, "Synthesising Controllers from RealTime Specifications," in Proc. Tenth International Symposium on System Synthesis, 1997, pp. 126133.
@inproceedings{hd97isss,
author = {Henning Dierks},
title = {{Synthesising Controllers from RealTime Specifications}},
booktitle = {{Tenth International Symposium on System Synthesis}},
year = {1997},
publisher = {IEEE CS Press},
optmonth = sep, pages = {126133},
publists = {Mobybg},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hd97isss.ps.gz} } 
[inproceedings] bibtex  Go to documentH. Fleischhack and J. Tapken, "An MNet Semantics for a RealTime Extension of $\mu$SDL," in Proc. Formal Methods: Their Industrial Application and Strengthened Foundations (FME'97), 1997, pp. 162181.
@inproceedings{hfjt97,
author = {Hans Fleischhack and Josef Tapken},
title = {An {MNet} Semantics for a RealTime Extension of {$\mu$SDL}},
booktitle = {Formal Methods: Their Industrial Application and Strengthened Foundations (FME'97)},
publisher = springer, series = lncs, volume = 1313, year = 1997, pages = {162181},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hfjt97.ps.gz} } 
[inproceedings] bibtexC. Fischer, "Combining ObjectZ and CSP," in Proc. Formale Beschreibungstechniken für verteilte Systeme, GI/ITGFachgespräch, 19.20. Juni 1997 in Berlin, 1997, pp. 119128.
@inproceedings{cf97gi,
author = {Clemens Fischer},
title = {Combining {ObjectZ} and {CSP}},
booktitle = {Formale Beschreibungstechniken f{\"u}r verteilte Systeme, GI/ITGFachgespr\"ach, 19.20. Juni 1997 in Berlin},
editor = {A. Wolisz and I. Schieferdecker and A. Rennoch},
publisher = {GMDForschungszentrum Informationstechnik GMBH},
series = {GMDStudien},
number = 315, year = 1997, pages = {119128},
note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/cf97gia.ps.gz} {An abstract is available online}} } 
[inproceedings] bibtexC. Fischer, "CSPOZ: A Combination of ObjectZ and CSP," in Proc. Formal Methods for Open ObjectBased Distributed Systems (FMOODS '97), 1997, pp. 423438.
@inproceedings{cf97,
author = {Clemens Fischer},
title = {{CSPOZ}: A Combination of {ObjectZ} and {CSP}},
booktitle = {Formal Methods for Open ObjectBased Distributed Systems (FMOODS '97)},
year = 1997, volume = 2, editor = {H. Bowmann and J. Derrick},
publisher = {Chapman \& Hall},
pages = {423438},
publists = {cspoz},
optnote = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/cf97a.ps.gz} {An abstract is available online}},
abstract = { In this paper we define a combination of ObjectZ and CSP called CSPOZ. The basic idea is to define a CSPsemantics for every ObjectZ class. Special care is taken to capture the characteristics of input and output parameters properly and to preserve the expected refinement rules. CSPOZ is well suited for the specification and development of communicating distributed systems. It provides powerful techniques to model data and controlaspects in a common framework. The language is easy to use for Z and ObjectZ users. } } 
[inproceedings] bibtex  Go to documentH. Dierks, "PLCAutomata: A New Class of Implementable RealTime Automata," in Proc. TransformationBased Reactive Systems Development (ARTS'97), 1997, pp. 111125.
@inproceedings{hd97arts,
author = {Henning Dierks},
title = {{PLCAutomata: A New Class of Implementable RealTime Automata}},
booktitle = {TransformationBased Reactive Systems Development (ARTS'97)},
editor = {M. Bertran and T. Rus},
series = lncs, volume = {1231},
year = {1997},
publisher = springer, pages = {111125},
publists = {Mobybg},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hd97arts.ps.gz} } 
[inproceedings] bibtex  Go to documentS. Kleuker, "Formalizing Requirements for Distributed Systems with Trace Diagrams," in Proc. Formal Methods: Their Industrial Application and Strengthened Foundations (FME'97), 1997, pp. 102121.
@inproceedings{sk97fme,
author = {Stephan Kleuker},
title = {Formalizing Requirements for Distributed Systems with Trace Diagrams},
booktitle = {Formal Methods: Their Industrial Application and Strengthened Foundations (FME'97)},
editor = {J. Fitzgerald and C.B. Jones and P. Lucas},
publisher = springer, series = lncs, volume = 1313, year = 1997, pages = {102121},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/sk97fme.ps.gz},
publists = {skleuker} } 
[inproceedings] bibtex  Go to documentS. Kleuker, "Anforderungsformalisierung für synchron kommunizierende Prozesse mit TraceDiagrammen," in Proc. Formale Beschreibungstechniken für verteilte Systeme, GI/ITGFachgespräch, 19.20. Juni 1997 in Berlin, 1997, pp. 175184.
@inproceedings{sk97gi,
author = {Stephan Kleuker},
title = {{A}nforderungsformalisierung f{\"u}r synchron kommunizierende {P}rozesse mit {T}race{D}iagrammen},
booktitle = {Formale Beschreibungstechniken f{\"u}r verteilte Systeme, GI/ITGFachgespr\"ach, 19.20. Juni 1997 in Berlin},
editor = {A. Wolisz and I. Schieferdecker and A. Rennoch},
publisher = {GMDForschungszentrum Informationstechnik GMBH},
series = {GMDStudien},
volume = 315, year = 1997, pages = {175184},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/sk97gi.ps.gz},
publists = {skleuker} } 
[inproceedings] bibtex  Go to documentH. Dierks and C. Dietz, "Graphical Specification and Reasoning: Case Study "Generalized Railroad Crossing"," in Proc. FME'97, 1997, pp. 2039.
@inproceedings{hdcd97,
author = {Henning Dierks and Cheryl Dietz},
title = {{Graphical Specification and Reasoning: Case Study "Generalized Railroad Crossing"}},
booktitle = {FME'97},
optcrossref = {LNCS1313},
editor = {J. Fitzgerald and C.B. Jones and P. Lucas},
volume = 1313, series = lncs, year = 1997, publisher = springer, pages = {2039},
publists = {Mobybg},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/hdcd97fme.ps.gz} } 
[inproceedings] bibtex  Go to documentS. Kleuker, "Incremental Development of DeadlockFree Communicating Systems," in Proc. Proceedings of the Third International Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), 1997, pp. 306320.
@inproceedings{sk97tacas,
author = {Stephan Kleuker},
title = {Incremental Development of DeadlockFree Communicating Systems},
booktitle = {Proceedings of the Third International Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97)},
editor = {E. Brinksma},
publisher = springer, series = lncs, volume = {1217},
year = 1997, pages = {306320},
abstract = { A basic property which distributed communicating systems have to fulfill is deadlockfreedom. For systems consisting of the parallel composition of subsystems it is complex to check deadlockfreedom because the global state space of the composition has to be investigated. This paper presents an approach by which the absence of deadlocks is preserved during the development. Small initial deadlockfree systems are stepwise extended with new functionalities to large complex systems by transformation rules which preserve deadlockfreedom. Systems are represented by finite automata extended with arbitrary local variables. A verification rule is presented which ensures that the parallel composition of such extended automata is deadlockfree. The advantage of this rule is that only information over pairs of connected subsystems is needed and not over the complete state space. },
publists = {skleuker},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/sk97tacas.ps.gz} } 
[inproceedings] bibtexC. Dietz, "Action Diagrams," in Proc. Proceedings of the IFAC/IFIP Workshop, Lyon, France, 1517 September 1997, 1997.
@inproceedings{cd97,
author = {Cheryl Dietz},
title = {{Action Diagrams}},
booktitle = {Proceedings of the IFAC/IFIP Workshop, Lyon, France, 1517 September 1997},
editor = {Mathieu Maranzana},
volume = {RealTime Programming 1997},
pages = {},
address = {},
series = {},
publisher = {Elsevier Science 1998},
comments = {},
month = {},
organization = {},
year = {1997},
note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/cd97a.ps.gz} {An abstract is available online}} } 
[techreport] bibtexH. Fleischhack and B. Grahlmann, "A Petri Net semantics for B(PN)$^2$ with procedures which allow verification," University of Hildesheim, Germany, InformatikBerichte 21/96, 1996.
@techreport{hfbg96,
author = {Hans Fleischhack and Bernd Grahlmann},
title = {A {P}etri {N}et semantics for {B(PN)$^2$} with procedures which allow verification},
institution = {University of Hildesheim, Germany},
year = 1996, type = {InformatikBerichte},
number = {21/96} } 
[inproceedings] bibtexS. Kleuker, "Using Formal Methods in the Development of Protocols for MultiUser Multimedia Systems," in Proc. Proceedings of the 9th international conference on Formal Description Techniques (FORTE'96) (Kaiserslautern, Germany), 1996, pp. 113128.
@inproceedings{sk96forte,
author = {Stephan Kleuker},
title = {Using Formal Methods in the Development of Protocols for MultiUser Multimedia Systems},
booktitle = {Proceedings of the 9th international conference on Formal Description Techniques (FORTE'96) (Kaiserslautern, Germany)},
editor = {R. Gotzhein and J. Bredereke},
year = 1996, publisher = {Chapman \& Hall},
publists = {skleuker},
pages = {113128} } 
[inproceedings] bibtex  Go to documentJ. Bohn and W. Janssen, "A Strategic Approach to Transformational Design," in Proc. Industrial Benefit and Advances in Formal Methods (FME'96), 1996, pp. 609628.
@inproceedings{jbwj96,
author = { J{\"u}rgen Bohn and Wil Janssen },
title = { A Strategic Approach to Transformational Design },
booktitle = {Industrial Benefit and Advances in Formal Methods (FME'96)},
volume = 1051, pages = {609628},
series = lncs, publisher = springer, year = 1996, url = {http://csd.informatik.unioldenburg.de/pub/Papers/jbwj96fme.ps.gz} } 
[inproceedings] bibtexC. Dietz, "Graphical Formalization of RealTime Requirements," in Proc. Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'96) (Uppsala, Sweden), 1996, pp. 366385.
@inproceedings{cd96,
author = {Cheryl Dietz},
title = {Graphical Formalization of RealTime Requirements},
booktitle = {Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'96) (Uppsala, Sweden)},
editor = {B. Jonsson and J. Parrow},
volume = {1135},
series = lncs, publisher = springer, year = 1996, pages = {366385},
note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/cd96ea.ps.gz} {An extended abstract is available online}} } 
[inproceedings] bibtexC. Fischer and W. Janssen, "Synchronous Development of Asynchronous Systems," in Proc. Proceedings of CONCUR'96, 1996, pp. 735750.
@inproceedings{cfwj96,
author = {Clemens Fischer and Wil Janssen},
title = {Synchronous Development of Asynchronous Systems},
booktitle = {Proceedings of CONCUR'96},
editor = {Ugo Montanari and Vladimiro Sassone},
volume = {1119},
series = lncs, publisher = springer, year = 1996, pages = {735750},
note = {\url{http://csd.informatik.unioldenburg.de/pub/CoCoN/cfwj96a.ps.gz} {An abstract is available online}} } 
[inproceedings] bibtex  Go to documentH. Dierks, "The Production Cell: A Verified RealTime System," in Proc. Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'96) (Uppsala, Sweden), 1996, pp. 208227.
@inproceedings{hd96,
author = {Henning Dierks},
title = {The Production Cell: A Verified RealTime System},
booktitle = {Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'96) (Uppsala, Sweden)},
editor = {B. Jonsson and J. Parrow},
volume = {1135},
series = lncs, publisher = springer, year = 1996, pages = {208227},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/FTRTFT96.ps.gz} } 
[inproceedings] bibtex  Go to documentM. Schenke and A. P. Ravn, "Refinement from a control problem to programs," in Proc. Formal methods for industrial applications: specifying and programming the steam boiler control, 1996, pp. 403427.
@inproceedings{ms96,
author = {Michael Schenke and A. P. Ravn},
title = {Refinement from a control problem to programs},
booktitle = {Formal methods for industrial applications: specifying and programming the steam boiler control},
editor = {JeanRaymond Abrial and Egon Borger and Hans Langmaack},
volume = 1165, series = lncs, year = 1996, publisher = springer, pages = {403427},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ms96.ps.gz} } 
[inproceedings] bibtex  Go to documentS. Kleuker, "The Extension of Existing Telecommunication Software with new Services Using Formal Methods," in Proc. Proceedings of the International Workshop on Advanced Intelligent Networks, 1996, pp. 91106.
@inproceedings{sk96ain,
author = {Stephan Kleuker},
title = {The Extension of Existing Telecommunication Software with new Services Using Formal Methods},
editor = {T. Margaria},
booktitle = {Proceedings of the International Workshop on Advanced Intelligent Networks},
publisher = {University of Passau},
year = 1996, pages = {91106},
url = {http://csd.informatik.unioldenburg.de/pub/CoCoN/sk96ain.ps.gz},
publists = {skleuker},
abstract = { Software development based on formal methods is a rigorous approach to provably correct software. A problem is that for most industrial applications the system development never terminates because requirements change and new functionality has to be added to the system. One typical example are telecommunication systems with a permanently increasing number of new services that have to be supported. Therefore the formal development of extensible and correct specifications becomes more and more important. But extensibility is not treated in formal methods so far. This paper describes an approach for the development of extensible specifications in small intuitive steps for communication networks at different levels of abstraction. } } 
[techreport] bibtex  Go to documentS. Kleuker and H. Tjabben, "A Formal Approach to the Development of Reliable MultiUser Multimedia Communication Systems," Philips Research Laboratories Aachen, Germany, Technical Report 1168/96, 1996.
@techreport{sk96philips,
author = {S. Kleuker and H. Tjabben },
title = {A Formal Approach to the Development of Reliable MultiUser Multimedia Communication Systems },
type = {Technical Report},
number = {1168/96},
institution = {Philips Research Laboratories Aachen },
address = {Germany},
year = 1996, url = {http://csd.informatik.unioldenburg.de/pub/CoCoN/sk96philips.ps.gz},
publists = {skleuker},
abstract = { Multiuser multimedia communication systems allow users at different sites to exchange any kind of information (video, audio and data) in a multipoint call. A typical application area for such systems can be hospitals. Especially the medical area poses strong requirements on the reliability and security of the communication systems and of the application software. This paper presents an approach how formal methods can help to meet these requirements. The first part of this paper gives a short introduction to a set of standards for multipoint communications recently proposed by the ITUT (International Telecommunications Union  Telecommunications Standardization Sector). Only parts of these standards contain formal specifications while others contain only informal textual descriptions. The second part begins with the development of a simple formal specification of a multiuser multimedia communication system based on these standards. We start by collecting informal requirements for conference handling as the basic functionality of the system aimed at. These requirements are formalized and a specification is developed for which we prove that it is in accordance with the requirements. It is then explained how new functionality can be added with an incremental development technique. This technique supports that unchanged requirements remain valid in the new system. Stepwise employing of this technique leads from our initial specification to more enhanced and complete formal specifications. In the end we sketch how the final specification can be used for the development of new applications for multiuser multimedia communication systems. These applications are realized on top of a system with proven properties and therefore we can guarantee their correctness. Work presented in this paper is done as part of the project CoCoN (Provably Correct Communication Networks) that is carried out in cooperation between the Philips Research Laboratories in Aachen and the University of Oldenburg. } } 
[incollection] bibtexE. R. Olderog, A. P. Ravn, and J. U. Skakkebæk, "Refining System Requirements to Program Specifications," in Formal Methods for RealTime Computing, Heitmeyer, C. and Mandrioli, D., Eds., Wiley, 1996, vol. 5, pp. 107134.
@incollection{ero96,
author = {E.R. Olderog and A. P. Ravn and J. U. Skakkeb{\ae}k},
title = {Refining System Requirements to Program Specifications},
editor = {C. Heitmeyer and D. Mandrioli},
booktitle = {Formal Methods for RealTime Computing},
chapter = 5, pages = {107134},
publisher = {Wiley},
series = {Trends in Software},
volume = 5, year = 1996, note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/ero96.ps.gz} {An abstract is available online}} } 
[inproceedings] bibtex  Go to documentS. Kleuker and H. Tjabben, "The Incremental Development of Correct Specifications for Distributed Systems," in Proc. Industrial Benefit and Advances in Formal Methods (FME'96), 1996, pp. 479498.
@inproceedings{sk96fme,
author = {S. Kleuker and H. Tjabben},
title = {The Incremental Development of Correct Specifications for Distributed Systems},
editor = {M.C. Gaudel and J. Woodcock},
booktitle = {Industrial Benefit and Advances in Formal Methods (FME'96)},
publisher = springer, series = lncs, volume = 1051, year = 1996, pages = {479498},
url = {http://csd.informatik.unioldenburg.de/pub/CoCoN/sk96fme.ps.gz},
publists = {skleuker},
abstract = { Provably correct software can only be achieved by basing the development process on formal methods. For most industrial applications such a development never terminates because requirements change and new functionality has to be added to the system. Therefore a formal method that supports an incremental development of complex systems is required. The project CoCoN (Provably Correct Communication Networks) that is carried out jointly between Philips Research Laboratories Aachen and the University of Oldenburg takes results from the ESPRIT Basic Research Action ProCoS to show the applicability of a more formal approach to the development of correct telecommunications software. These ProCoSmethods have been adapted to support the development of extensible specifications for distributed systems. Throughout this paper our approach is exemplified by a case study how call handling software for telecommunication switching systems should be developed. } } 
[techreport] bibtexJ. Bohn and W. Janssen, "From a Single Specification to Many Implementations  Many roads lead to parallelism," uniolfb101995.
@techreport{jbwj95,
author = {J. Bohn and W. Janssen},
title = {From a Single Specification to Many Implementations  Many roads lead to parallelism},
institution = uniolfb10, year = 1995 } 
[mastersthesis] bibtexR. Müller, "An\forderungs\ger\echte Spez\ifika\tion eines zeit\ab\hän\gigen Gebüh\renab\rech\nungs\systems," Master's Dissertation , 1995.
@mastersthesis{rm95,
author = {R. M\"uller},
title = {{A}n\forderungs\ger\echte {S}pez\ifika\tion eines zeit\ab\h\"an\gigen {G}eb\"uh\renab\rech\nungs\systems},
school = uniolfb10, month = apr, year = 1995 } 
[inproceedings] bibtex  Go to documentH. Tjabben, S. Kleuker, and A. Kehne, "Provably Correct Intelligent Networks," in Proc. Proceedings of the IEEE Intelligent Network '95 Workshop, May 911, 1995, Ottawa, Canada, 1995.
@inproceedings{sk95ieee,
author = {H. Tjabben and S. Kleuker and A. Kehne},
title = {Provably Correct Intelligent Networks},
booktitle = {Proceedings of the IEEE Intelligent Network '95 Workshop, May 911, 1995, Ottawa, Canada },
year = 1995, publists = {skleuker},
url = {http://csd.informatik.unioldenburg.de/pub/CoCoN/sk95ieee.ps.gz} } 
[techreport] bibtexE. Best and H. F. (Ed.), "PEP: Programming Environment based on Petri Nets," University of Hildesheim, Germany, InformatikBerichte 14/95, 1995.
@techreport{ebhf95hi,
author = {Eike Best and Hans Fleischhack (Ed.)},
title = {{PEP: Programming Environment based on Petri Nets}},
institution = {University of Hildesheim, Germany},
year = 1995, type = {InformatikBerichte},
number = {14/95} } 
[inproceedings] bibtexE. Best, H. Fleischhack, W. Fraczak, R. P. Hopkins, H. Klaudel, and E. Pelz, "An MNet semantics of B(PN)$^2$.," in Proc. Structures in Concurrency Theory, 1995.
@inproceedings{ebhf95wics,
author = {Eike Best and Hans Fleischhack and W. Fraczak and R. P. Hopkins and H. Klaudel and E. Pelz},
title = {An {MNet} semantics of {B(PN)$^2$}.},
editor = {J. Desel},
booktitle = {Structures in Concurrency Theory},
publisher = springer, series = wics, year = 1995 } 
[techreport] bibtex  Go to documentJ. Bohn and S. Rössig, "On Automatic and Interactive Design of Communicating Systems," uniolfb10, ProCoS Document [OLD JB 2/2], 1995.
@techreport{jbsr95procos2,
author = { J{\"u}rgen Bohn and Stephan R{\"o}ssig },
title = { On Automatic and Interactive Design of Communicating Systems },
institution = uniolfb10, type = { ProCoS Document },
number = {[OLD JB 2/2]},
year = 1995, url = {http://csd.informatik.unioldenburg.de/pub/ProCoS/JB22.ps.gz} } 
[techreport] bibtex  Go to documentJ. Bohn and S. Rössig, "Towards a Design Assistant for Communicating Systems," uniolfb10, ProCoS Document [OLD JB 3/1], 1995.
@techreport{jbsr95procos3,
author = { J{\"u}rgen Bohn and Stephan R{\"o}ssig },
title = { Towards a Design Assistant for Communicating Systems },
institution = uniolfb10, type = { ProCoS Document },
number = {[OLD JB 3/1]},
year = 1995, url = {http://csd.informatik.unioldenburg.de/pub/ProCoS/JB31.ps.gz} } 
[article] bibtexJ. Bohn and H. Hungar, "Traverdi  Transformation and Verification of Distributed Systems," lncs, vol. 1009, pp. 317???, 1995.
@article{jbhh95,
author = { J{\"u}rgen Bohn and Hardi Hungar },
title = { Traverdi  Transformation and Verification of Distributed Systems },
journal = lncs, pages = {317???{}},
editor = { M. Broy and S. J\"anichen },
publisher = springer, volume = 1009, year = 1995 } 
[techreport] bibtex  Go to documentC. Fischer, "Semantics and Compositional Verification of $\mu$SDL," Philips Research Laboratories Aachen, Germany, Labornotiz 1/95, 1995.
@techreport{cf95philips,
author = {Clemens Fischer},
title = {Semantics and Compositional Verification of {$\mu$SDL}},
institution = {Philips Research Laboratories Aachen },
address = {Germany},
year = 1995, type = {Labornotiz},
number = {1/95},
url = {http://csd.informatik.unioldenburg.de/pub/CoCoN/cf95philips.ps.gz} } 
[inproceedings] bibtexA. Gronewold and H. Fleischhack, "Computing Petri Net Languages by Reductions," in Proc. Proceedings on the 10th International Conference on Fundamentals of computation theory (FCT'95) (Dresden, Germany, August 1995), 1995, pp. 253???.
@inproceedings{aghf95, editor = {Horst Reichel},
booktitle = {Proceedings on the 10th International Conference on Fundamentals of computation theory ({FCT}'95) (Dresden, Germany, August 1995)},
author = {A. Gronewold and Hans Fleischhack},
title = {Computing {Petri} Net Languages by Reductions},
series = lncs, volume = {965},
pages = {253???{}},
year = {1995},
publisher = springer } 
[inproceedings] bibtexE. Best, H. Fleischack, W. Fraczak, and R. P. Hopkins, "A Class of Composable High Level Petri Nets with an Application to the Semantics of B(PN)$^2$," in Proc. Proceedings of the 16th Internationcal Conference on Application and Theory of Petri nets (Turin, Italy, June 2630, 1995), 1995, pp. 103118.
@inproceedings{ebhf95lncs, editor = {Giorgio De Michelis and Michel Diaz},
booktitle = {Proceedings of the 16th Internationcal Conference on Application and Theory of Petri nets (Turin, Italy, June 2630, 1995)},
author = {E. Best and Hans Fleischack and W. Fraczak and R. P. Hopkins},
title = {A Class of Composable High Level {Petri} Nets with an Application to the Semantics of {B(PN)$^2$}},
series = lncs, volume = {935},
publisher = springer, pages = {103118},
year = {1995} } 
[inproceedings] bibtex  Go to documentE. R. Olderog and M. Schenke, "Design of RealTime Systems: The Interface between Duration Calculus and Program Specifications," in Proc. Structures in Concurrency Theory, 1995, pp. 3254.
@inproceedings{eroms95,
author = {E.R. Olderog and M. Schenke},
title = {Design of RealTime Systems: The Interface between Duration Calculus and Program Specifications},
editor = {J. Desel},
booktitle = {Structures in Concurrency Theory},
publisher = springer, series = wics, year = 1995, pages = {3254},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/eroms95.ps.gz} } 
[inproceedings] bibtexH. Fleischhack and J. Tapken, "Eine kompositionelle PetrinetzSemantik für SDLSpezifikationen," in Proc. 2. Workshop Algorithmen und Werkzeuge für Petrinetze, 1995.
@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} } 
[inproceedings] bibtexJ. Bohn and S. Rössig, "On Automatic and Interactive Design of Communicating Systems," in Proc. Proceedings of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95) (Aarhus, Denmark), 1995, pp. 216237.
@inproceedings{jbsr95tacas,
author = {J{\"u}rgen Bohn and Stephan R{\"o}ssig},
title = {On Automatic and Interactive Design of Communicating Systems},
editor = {E. Brinksma and W. R. Cleaveland and K. G. Larsen and T. Margaria and B. Steffen},
booktitle = {Proceedings of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95) (Aarhus, Denmark)},
series = lncs, volume = 1019, pages = {216237},
publisher = springer, year = 1995, abstract = { The design of provable correct software requires formal methods whose usage should be assisted by suitable tools. Following a transformational approach the design needs interactive user help when important design decisions have to be made. Nevertheless simple parts should be automated as far as possible. Ideally the user only guides the design process by indicating the design ideas which are then carried out automatically. Typically sequential implementations are more appropriate for automation while parallelization needs interaction to determine the intended program architecture.\bibpar This paper presents a transformational approach to the design of distributed systems where environment and concurrently running components communicate via synchronous message passing along directed channels. System specifications that combine tracebased with statebased reasoning are gradually modified by application of transfromation rules until Occamlike programs are achieved finally. We consider interactive and automatic aspects of such a design process and illustrate our approach by sketching the development of a shared register implementation. } } 
[inproceedings] bibtex  Go to documentS. Kleuker and H. Tjabben, "A Formal Approach to the Development of Reliable MultiUser Multimedia Applications," in Proc. Proceedings of the 5th GI/ITGFachgespräch ``Formale Beschreibungs\techniken für verteilte Systeme'', 1995, pp. 110.
@inproceedings{sk95gi,
author = {S. Kleuker and H. Tjabben},
title = {A Formal Approach to the Development of Reliable MultiUser Multimedia Applications },
editor = {R. Gotzhein and J. Bredereke },
booktitle = {Proceedings of the 5th GI/ITGFachgespr\"ach ``Formale Beschreibungs\techniken f\"ur verteilte Systeme'' },
publisher = {University of Kaiserslautern, Department of Computer Science},
year = 1995, pages = {110},
url = {http://csd.informatik.unioldenburg.de/pub/CoCoN/sk95gi.ps.gz},
abstract = { Multiuser multimedia communication systems allow users at different sides to exchange any kind of information (video, audio and data) in a multipoint call. We expect that these systems will at first be used in professional areas like hospitals. The medical area poses strong requirements on the reliability and security of the application software. This paper presents an approach how formal methods can help to meet these requirements. },
publists = {skleuker} } 
[techreport] bibtex  Go to documentS. Kleuker, A. Kehne, and H. Tjabben, "Provably Correct Communication Networks (CoCoN)," Philips Research Laboratories Aachen, Germany, Technical Report 1123/95, 1995.
@techreport{sk95philips,
author = {S. Kleuker and A. Kehne and H. Tjabben },
title = {Provably Correct Communication Networks ({CoCoN}) },
type = {Technical Report},
number = {1123/95 },
institution = {Philips Research Laboratories Aachen },
address = {Germany},
year = 1995, url = {http://csd.informatik.unioldenburg.de/pub/CoCoN/sk95philips.ps.gz},
publists = {skleuker},
abstract = { During the last few years there has been an ever increasing demand for the fast and flexible introduction of valueadded services and new features into private as well as into public telecommunications networks. Intelligent networks (IN), personal communications, computersupported telecommunications applications (CSTA) are just a few areas from which these services are emerging. Adding more and more services to the telecommunications network leads to a situation where not only the software part of the separate network components but also the structure of the network is becoming increasingly complex. Today, it is already difficult to maintain and to extend the systems. It becomes more and more harder to understand and to predict the behaviour of the system, e.g. in situations when interactions between services occur. Therefore it becomes a key issue to design communications system software that provably not only arguably meets its requirements. Aim of our project is to support a stepwise and verified development of communications systems from the requirement phase over the specification phase to an implementation. The vision that we have in mind is an engineering approach for the development of correct communications networks. Meanwhile theoretical work has reached a point where formal methods seem to be applicable to industrialsize applications. Here we would especially like to mention the ESPRIT Basic Research Project ProCoS (= Provably Correct Systems). This project was started in 1989 and finished in 1992, a followup project ProCoS II was initiated 1993. ProCoS is dedicated to cover the entire development process from the capture of the requirements down to the computer programs. ProCoS offers a constructive approach to correctness, that is based on a common mathematical model. Our project CoCoN is closely related to the ProCoS project. The formal methods that have been developed within the ProCoS framework establish the foundation of our approach. In particular, distributed embedded realtime systems are in the scope of ProCoS. Therefore the ProCoS methods are considered to be directly applicable to problems from the communications area. Call handling for the originating and terminating side in a plain network configuration is used as a consistent example throughout the whole report to describe the principles of our approach. We proceed in the following way: Informal requirements for basic call handling are first identified and then captured in a formal language. In a next step from these formal requirements a specification is developed and it is proved that the resulting specification is correct with respect to the requirements. It is then shown how it is possible to decompose the resulting small switching system specification in order to come to more realistic network configurations. New transformation rules are introduced. These rules enable the stepwise extension of the starting system into a complex but still verified system. } } 
[inproceedings] bibtex  Go to documentS. Kleuker, "A Gentle Introduction to Specification Engineering using a Case Study in Telecommunications," in Proc. International Joint Conference on Theory and Practice of Software Development (TAPSOFT'95), 1995, pp. 636650.
@inproceedings{sk95tapsoft,
author = {S. Kleuker},
title = {A Gentle Introduction to Specification Engineering using a Case Study in Telecommunications},
editor = {P. D. Mosses and M. Nielsen and M. I. Schwartzbach},
booktitle = {International Joint Conference on Theory and Practice of Software Development (TAPSOFT'95)},
publisher = springer, series = lncs, volume = 915, year = 1995, pages = {636650},
url = {http://csd.informatik.unioldenburg.de/pub/CoCoN/sk95tapsoft.ps.gz},
publists = {skleuker},
abstract = { Software development based on formal methods is the only way to provably correct software. Therefore a method for the development of complex systems in intuitive steps is needed. A suitable solution is the transformational approach where verified semanticspreserving transformation rules are used to come from a first verified specification to the desired system. A problem is that for most industrial applications the system development never terminates because requirements change and new functionalities have to be added to the system. This paper describes a new approach for the development of extensible specifications in small intuitive steps. New transformation rules are introduced that guarantee that intermediate results of development can be used for further steps. } } 
[misc] bibtexJ. Bohn, Formal Reasoning about Specification and Transformation of Reactive Systems, 1994.
@misc{jb94,
author = { J{\"u}rgen Bohn },
title = { Formal Reasoning about Specification and Transformation of Reactive Systems },
year = 1994, note = {Draft version} } 
[book] bibtexK. R. Apt and E. R. Olderog, Programmverifikation, springer, 1994.
@book{ero94,
author = {K. R. Apt and E.R. Olderog},
title = {Programmverifikation},
publisher = springer, note = {{\url{http://csd.Informatik.UniOldenburg.DE/~skript/pub/Papers/Errata.ps} {ErrataListe}} bzw. {\url{http://csd.Informatik.UniOldenburg.DE/~skript/pub/Papers/Errata\_long.ps} {ErrataListe mit Tippfehlern}}},
year = 1994 } 
[phdthesis] bibtexS. Rössig, "A Transformational Approach to the Design of Communicating Systems," PhD Thesis , 1994.
@phdthesis{sr94phd,
author = {S. R\"ossig},
title = { A Transformational Approach to the Design of Communicating Systems},
school = uniolfb10, month = oct, year = 1994 } 
[inproceedings] bibtexJ. Bohn, "Formal Transformational Reasoning about Reactive Systems in the Theorem Prover LAMBDA," in Proc. Supplementary proceedings of the 7th international workshop on Higher Order Logic Theorem Proving and its Applications, 1994.
@inproceedings{jb94hol,
author = { J{\"u}rgen Bohn },
title = { Formal Transformational Reasoning about Reactive Systems in the Theorem Prover {LAMBDA} },
booktitle = { Supplementary proceedings of the 7th international workshop on Higher Order Logic Theorem Proving and its Applications },
year = 1994, editor = { T. Melham and J. Camilleri },
publisher = { University of Malta } } 
[techreport] bibtex  Go to documentJ. Bohn, "Formalizing the SL/PL design approach in LAMBDA," uniolfb10, ProCoS Document [OLD JB 1/1], 1994.
@techreport{jb94procos,
author = { J{\"u}rgen Bohn },
title = { Formalizing the {SL/PL} design approach in {LAMBDA} },
institution = uniolfb10, type = { ProCoS Document },
number = {[OLD JB 1/1]},
year = 1994, url = {http://csd.informatik.unioldenburg.de/pub/ProCoS/JB11.ps.gz} } 
[inproceedings] bibtexJ. He, C. A. R. Hoare, M. Fränzle, M. MüllerOlm, E. R. Olderog, M. Schenke, M. R. Hansen, A. P. Ravn, and H. Rischel, "Provably Correct Systems," in Proc. Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'94), 1994, pp. 288335.
@inproceedings{eroms94ftrtft,
author = {Jifeng He and C. A. R. Hoare and M. Fr\"anzle and M. M\"ullerOlm and E.R. Olderog and M. Schenke and M. R. Hansen and A. P. Ravn and H. Rischel},
title = {Provably Correct Systems},
editor = {H. Langmaack and W. P. {de Roever} and J. Vytopil},
booktitle = {Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'94)},
series = lncs, publisher = springer, year = 1994, volume = 863, pages = {288335} } 
[inproceedings] bibtex  Go to documentM. Schenke, "A Timed Specification Language for Concurrent Reactive Systems," in Proc. Semantics of Specification Languages, 1994, pp. 152167.
@inproceedings{ms94,
author = {M. Schenke},
title = {A Timed Specification Language for Concurrent Reactive Systems},
editor = { D. J. Andrews and J. F. Groote and C. A. Middelburg},
booktitle = {Semantics of Specification Languages},
series = wics, publisher = springer, year = 1994, pages = {152167},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ms94.ps.gz} } 
[inproceedings] bibtexC. Dietz and G. Schreiber, "A Term Representation of P/T systems," in Proc. Application and Theory of Petri Nets, 1994, pp. 239257.
@inproceedings{cd94,
author = {C. Dietz and G. Schreiber},
title = {A Term Representation of {P/T} systems},
booktitle = {Application and Theory of Petri Nets},
editor = {R. Valette},
volume = 815, series = lncs, year = 1994, publisher = springer, pages = {239257},
note = {\url{http://csd.informatik.unioldenburg.de/pub/Papers/cd94ea.ps.gz} {An extended abstract is available online}} } 
[inproceedings] bibtex  Go to documentM. Schenke, "Specification and Transformation of Reactive Systems with Time Restrictions and Concurrency," in Proc. Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'94), 1994, pp. 605621.
@inproceedings{ms94ftrtft,
author = {M. Schenke},
title = {Specification and Transformation of Reactive Systems with Time Restrictions and Concurrency},
booktitle = {Formal Techniques in RealTime and FaultTolerant Systems (FTRTFT'94)},
editor = {H. Langmaack and W.P. {de Roever} and J. Vytopil},
series = lncs, publisher = springer, year = 1994, volume = 863, pages = {605621},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/ms94ftrtft.ps.gz} } 
[inproceedings] bibtexS. Kleuker, "Case Study: Stepwise Refinement of a Communication Processor Using Trace Logic," in Proc. Semantics of Specification Languages, 1994, pp. 252269.
@inproceedings{sk94,
author = {S. Kleuker},
title = {Case Study: Stepwise Refinement of a Communication Processor Using Trace Logic},
booktitle = {Semantics of Specification Languages},
editor = {D. J. Andrews and J. F. Groote and C. A. Middelburg},
publisher = springer, series = wics, year = 1994, pages = {252269},
publists = {skleuker},
abstract = { This paper shows a stepwise development of a complex parallel system. Both the initial requirements and the subsequent design stages are formulated in trace logic and so every proof of correctness boils down to reasoning about trace predicates. The relation between trace logic and a program language is shown by a transformation from trace logic into a program specification language, called SL. The advantage is that a large set of verified SLspecifications can be automatically transformed into correct OCCAM programs. In contrast to trace logic, SLspecifications describe the process behaviour in more detail. } } 
[inproceedings] bibtexH. Fleischhack and U. Lichtblau, "MOBY  A tool for high level Petri Nets with objects," in Proc. Proceedings of the IEEESMC'93Conference (Le Touquet, France, 1993), 1993, pp. 644649.
@inproceedings{hf93ieee,
author = {Hans Fleischhack and Ulrike Lichtblau},
title = {{MOBY}  {A} tool for high level {P}etri {N}ets with objects},
booktitle = {Proceedings of the IEEESMC'93Conference (Le Touquet, France, 1993)},
pages = {644649},
year = 1993 } 
[inproceedings] bibtexJ. P. Bowen, M. Fränzle, E. R. Olderog, and A. P. Ravn, "Developing Correct Systems," in Proc. Proceedings of the 5th EUROMICRO Workshop on RealTime Systems (Oulu, Finland), 1993, pp. 176189.
@inproceedings{ero93,
author = {J. P. Bowen and M. Fr\"anzle and E.R. Olderog and A. P. Ravn},
title = {Developing Correct Systems},
booktitle = {Proceedings of the 5th EUROMICRO Workshop on RealTime Systems (Oulu, Finland)},
pages = {176189},
publisher = {IEEE Computer Society Press},
year = 1993 } 
[inproceedings] bibtexH. Fleischhack, U. Lichtblau, M. Sonnenschein, and R. Wieting, "Abstraktion und Zeitbegriff in höheren Netzen," in Proc. PetriNetze im Einsatz für Entwurf und Entwicklung von Informationssystemen, Berlin [u.a.], 1993.
@inproceedings{hf93,
author = {Hans Fleischhack and Ulrike Lichtblau and Michael Sonnenschein and Ralf Wie\ting},
title = {{A}bstraktion und {Z}eitbegriff in h\"oheren {N}etzen},
booktitle = {{P}etri{N}etze im {E}insatz f\"ur {E}ntwurf und {E}ntwicklung von {I}nformationssystemen},
editor = {G. Scheschonk},
address = {Berlin [u.a.]},
year = {1993} } 
[inproceedings] bibtexJ. Bohn, "Formalizing the Transformational Design of Communicating Systems in the Theorem Prover LAMBDA," in Proc. Higher Order Algebra, Logic and Term Rewriting (HOA'93), 1993.
@inproceedings{jb93hoa,
author = { J{\"u}rgen Bohn },
title = { Formalizing the Transformational Design of Communicating Systems in the Theorem Prover {LAMBDA} },
booktitle = { Higher Order Algebra, Logic and Term Rewriting (HOA'93)},
year = 1993, editor = {J. Heering and K. Meinke and B. M\"oller },
publisher = { CWI, Amsterdam, The Netherlands } } 
[unpublished] bibtexClemens Fischer, Fehleranalyse bei der Spezifikationsentwicklung von intelligenten Telefonnetzen, 1993.
@unpublished{cf93,
author = {Clemens Fischer},
title = {{Fehleranalyse bei der Spezifikationsentwicklung von intelligenten Telefonnetzen}},
year = 1993, month = nov, type = {Studienarbeit},
note = uniolfb10 } 
[inproceedings] bibtexJ. Bohn, "Interaktive Synthese kommunizierender Systeme mit LAMBDA," in Proc. Formale Methoden zum Entwurf korrekter Systeme, 1993.
@inproceedings{jb93gi,
author = { J{\"u}rgen Bohn },
title = { {I}nteraktive {S}ynthese kommunizierender {S}ysteme mit {LAMBDA}},
booktitle = { Formale Methoden zum Entwurf korrekter Systeme },
year = 1993, editor = { Th. Kropf and R. Kumar and D. Schmid },
organization = { GI/ITGWorkshop },
publisher = { University of Karlsruhe, Germany } } 
[techreport] bibtex  Go to documentM. R. Hansen, E. R. Olderog, M. Schenke, M. Fränzle, B. von Karger, M. MüllerOlm, and H. Rischel, "A Duration Calculus Semantics for RealTime Reactive Systems," uniolfb10, ProCoS II document [OLD MRH 1/1], 1993.
@techreport{eroms93,
author = {M. R. Hansen and E.R. Olderog and M. Schenke and M. Fr\"anzle and B. {von Karger} and M. M\"ullerOlm and H. Rischel},
title = {A {Duration Calculus} Semantics for RealTime Reactive Systems},
type = {ProCoS II document},
number = {[OLD MRH 1/1]},
institution = uniolfb10, month = sep, year = 1993, url = {http://csd.informatik.unioldenburg.de/pub/Papers/eroms93.ps.gz} } 
[inproceedings] bibtexE. R. Olderog and S. Rössig, "A Case Study in Transformational Design of Concurrent Systems," in Proc. Theory and Practice of Software Development (TAPSOFT'93), 1993, pp. 90104.
@inproceedings{erosr93,
author = {E.R. Olderog and S. R\"ossig},
title = {A Case Study in Transformational Design of Concurrent Systems},
editor = {M.C. Gaudel and J.P. Jouannaud},
booktitle = {Theory and Practice of Software Development (TAPSOFT'93)},
series = lncs, volume = 668, publisher = springer, year = 1993, pages = {90104} } 
[incollection] bibtexE. R. Olderog, "Systematic derivation of communicating programs," in Programming and Mathematical Method, Broy, M., Ed., springer, 1992, pp. 369407.
@incollection{ero92,
author = {E.R. Olderog},
title = {Systematic derivation of communicating programs},
booktitle = {Programming and Mathematical Method},
publisher = springer, year = 1992, editor = {M. Broy},
pages = {369407} } 
[inproceedings] bibtexE. R. Olderog, "Interfaces between Languages for Communicating Systems," in Proc. Automata, Languages and Programming. Proceedings of the 19th ICALP 1992, 1992, pp. 641655.
@inproceedings{ero92icalp,
author = {E.R. Olderog},
title = {Interfaces between Languages for Communicating Systems},
editor = {W. Kuich},
booktitle = {Automata, Languages and Programming. Proceedings of the 19th ICALP 1992},
series = lncs, volume = 623, publisher = springer, year = 1992, pages = {641655},
note = {Invited paper} } 
[inproceedings] bibtex  Go to documentM. Schenke, "Predicative Specification of Timed Processes," in Proc. RealTime: Theory in Practice, 1992, pp. 603617.
@inproceedings{ms92,
author = {M. Schenke},
title = {Predicative Specification of Timed Processes},
booktitle = {RealTime: Theory in Practice},
editor = {J. W. {de Bakker} and W.P. {de Roever} and G. Rozenberg},
series = lncs, publisher = springer, volume = 600, pages = {603617},
year = 1992, url = {http://csd.informatik.unioldenburg.de/pub/Papers/ms92.ps.gz} } 
[article] bibtexE. R. Olderog, "Correctness of Concurrent Processes," tcs, vol. 80, pp. 263288, 1991.
@article{ero91correctness,
author = {E.R. Olderog},
title = {Correctness of Concurrent Processes},
journal = tcs, year = 1991, volume = 80, pages = {263288} } 
[book] bibtex  Go to documentE. R. Olderog, Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship, Cambridge University Press, 1991.
@book{Old05nets,
author = {E.R. Olderog},
title = {Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship},
publisher = {Cambridge University Press},
year = 1991, pages = {267},
note = {Paperback Edition 2005},
url = {http://www.cambridge.org/de/academic/subjects/computerscience/programminglanguagesandappliedlogic/netstermsandformulasthreeviewsconcurrentprocessesandtheirrelationship} } 
[incollection] bibtexK. R. Apt and E. R. Olderog, "Introduction to Program Verification," in Formal Description of Programming Concepts, Neuhold, E. J. and Paul, M., Eds., springer, 1991, pp. 363429.
@incollection{ero91intro,
author = {K. R. Apt and E.R. Olderog},
title = {Introduction to Program Verification},
booktitle = {Formal Description of Programming Concepts},
series = {IFIP StateoftheArt Reports},
publisher = springer, year = 1991, editor = {E. J. Neuhold and M. Paul},
pages = {363429} } 
[inproceedings] bibtexE. R. Olderog and K. R. Apt, "Using transformations to verify parallel programs," in Proc. Algebraic Methods II: Theory, Tools and Applications, 1991, pp. 5581.
@inproceedings{ero91algebraic,
author = {E.R. Olderog and K. R. Apt},
title = {Using transformations to verify parallel programs},
booktitle = {Algebraic Methods II: Theory, Tools and Applications},
editor = {J. A. Bergstra and L. M. G. Feijs},
volume = 490, series = lncs, year = 1991, publisher = springer, pages = {5581} } 
[inproceedings] bibtexE. R. Olderog, "Towards a Design Calculus for Communicating Programs," in Proc. Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR'91) (Amsterdam, The Netherlands), 1991, pp. 6177.
@inproceedings{ero91concur,
author = {E.R. Olderog},
title = {Towards a Design Calculus for Communicating Programs},
booktitle = {Proceedings of the 2nd International Conference on Concurrency Theory (CONCUR'91) (Amsterdam, The Netherlands)},
editor = {J. C. M. Baeten and J. F. Groote},
volume = 527, series = lncs, year = 1991, publisher = springer, pages = {6177} } 
[inproceedings] bibtex  Go to documentS. Rössig and M. Schenke, "Specification and Stepwise Development of Communicating Systems," in Proc. Formal Software Development Methods (VDM'91), 1991, pp. 149163.
@inproceedings{srms91,
author = {S. R\"ossig and M. Schenke},
title = {Specification and Stepwise Development of Communicating Systems},
booktitle = {Formal Software Development Methods (VDM'91)},
editor = {S. Prehn and W. J. Toetenel},
volume = 551, series = lncs, year = 1991, publisher = springer, pages = {149163},
url = {http://csd.informatik.unioldenburg.de/pub/Papers/srms91.ps.gz} } 
[article] bibtexC. J. J. Meyer and E. R. Olderog, "Hiding in Stream Semantics of Uniform Concurrency," acta, vol. 27, pp. 381397, 1990.
@article{ero90acta,
author = {J.J. Ch. Meyer and E.R. Olderog},
title = {Hiding in Stream Semantics of Uniform Concurrency},
journal = acta, year = 1990, volume = 27, pages = {381397} } 
[incollection] bibtexK. R. Apt, F. S. de Boer, and E. R. Olderog, "Proving termination of parallel programs," in Beauty is our Business  A Birthday Salute to Edsger W. Dijkstra, Feijen, W. H. J., van Gasteren, A. J. M., Gries, D., and Misra, J., Eds., springer, 1990.
@incollection{ero90dijkstra,
author = {K. R. Apt and F. S. {de Boer} and E.R. Olderog},
title = {Proving termination of parallel programs},
booktitle = {Beauty is our Business  A Birthday Salute to Edsger W. Dijkstra},
publisher = springer, year = 1990, editor = {W. H. J. Feijen and A. J. M. {van Gasteren} and D. Gries and J. Misra} } 
[incollection] bibtexE. R. Olderog, "From trace specifications to process terms," in Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, de Bakker, J. W., de Roever, W. P., and Rozenberg, G., Eds., springer, 1990, vol. 430, pp. 592621.
@incollection{ero90,
author = {E.R. Olderog},
title = {From trace specifications to process terms},
booktitle = {Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness},
publisher = springer, year = 1990, editor = {J. W. {de Bakker} and W.P. {de Roever} and G. Rozenberg},
volume = 430, series = lncs, pages = {592621} } 
[article] bibtexB. D., C. A. R. \. Hoare, J. P. Bowen, He Jifeng, H. Langmaack, E. R. Olderog, U. H. Martin, V. Stavridou, F. Nielson, H. R. Nielson, H. Barringer, D. Edwards, H. H. Lø., A. P. Ravn, and H. S. Rischel, "A ProCoS Project Description," Bulletin of the European Association for Theoretical Computer Science (EATCS), vol. 39, pp. 6073, 1989.
@article{ero89, title = {A {ProCoS} Project Description},
author = {D. Bj\o{}rner and C. A. R.\ Hoare and J. P. Bowen and {He Jifeng} and H. Langmaack and E.R. Olderog and U. H. Martin and V. Stavridou and F. Nielson and H. R. Nielson and H. Barringer and D. Edwards and H. H. L\o{}vengreen and A. P. Ravn and H. S. Rischel},
journal = {Bulletin of the European Association for Theoretical Computer Science (EATCS)},
volume = 39, pages = {6073},
month = {October},
year = 1989 } 
[article] bibtexJ. W. de Bakker, C. J. J. Meyer, E. R. Olderog, and J. I. Zucker, "Transition Systems, Metric Spaces and Ready Sets in the Semantics of Uniform Concurrency," jcss, vol. 36, pp. 158224, 1988.
@article{ero88jcss,
author = {J. W. {de Bakker} and J.J. Ch. Meyer and E.R. Olderog and J. I. Zucker},
title = {Transition Systems, Metric Spaces and Ready Sets in the Semantics of Uniform Concurrency},
journal = jcss, year = 1988, volume = 36, pages = {158224} } 
[article] bibtexJ. A. Bergstra, J. W. Klop, and E. R. Olderog, "Readies and Failures in the Algebra of Communicating Processes," siam, vol. 17, pp. 11341177, 1988.
@article{ero88siam,
author = {J. A. Bergstra and J. W. Klop and E.R. Olderog},
title = {Readies and Failures in the Algebra of Communicating Processes},
journal = siam, year = 1988, volume = 17, pages = {11341177} } 
[article] bibtexE. R. Olderog and K. R. Apt, "Fairness in Parallel Programs: the Transformational Approach," acmtoplas, vol. 10, pp. 420455, 1988.
@article{ero88toplas,
author = {E.R. Olderog and K. R. Apt},
title = {Fairness in Parallel Programs: the Transformational Approach},
journal = acmtoplas, year = 1988, volume = 10, pages = {420455} } 
[article] bibtexJ. W. de Bakker, C. J. J. Meyer, and E. R. Olderog, "Infinite Streams and Finite Observations in the Semantics of Uniform Concurrence," tcs, vol. 49, pp. 87112, 1987.
@article{ero87,
author = {J. W. de Bakker and J.J. Ch. Meyer and E.R. Olderog},
title = {Infinite Streams and Finite Observations in the Semantics of Uniform Concurrence},
journal = tcs, year = 1987, volume = 49, pages = {87112} } 
[inproceedings] bibtexJ. A. Bergstra, J. W. Klop, and E. R. Olderog, "Failures without Chaos: a Process Semantics for Fair Abstraction," in Proc. Formal Description of Programming Concepts  III, Amsterdam, 1987, pp. 77101.
@inproceedings{bko87,
author = {J.A. Bergstra and J.W. Klop and E.R. Olderog},
title = {Failures without Chaos: a Process Semantics for Fair Abstraction},
booktitle = {Formal Description of Programming Concepts  III},
editor = {M. Wirsing},
series = {Lecture Notes in Computer Science},
year = {1987},
publisher = {NorthHolland},
address = {Amsterdam},
pages = {77101} } 
[article] bibtexE. R. Olderog and C. A. R. Hoare, "Specificationoriented Semantics for Communicating Processes," acta, vol. 23, pp. 966, 1986.
@article{ero86,
author = {E.R. Olderog and C. A. R. Hoare},
title = {Specificationoriented Semantics for Communicating Processes},
journal = acta, year = 1986, volume = 23, pages = {966} } 
[inproceedings] bibtexJ. W. de Bakker, C. J. J. Meyer, E. R. Olderog, and J. I. Zucker, "Transition systems, infinitary languages and the semantics of uniform concurrency," in Proc. Proc.~17th ACM Symp.~on Theory of Computing, 1985, pp. 252262.
@inproceedings{bmoz85,
author = {J.W. de Bakker and J.J. Ch. Meyer and E.R. Olderog and J.I. Zucker},
title = {Transition systems, infinitary languages and the semantics of uniform concurrency},
booktitle = {Proc.~17th ACM Symp.~on Theory of Computing},
year = {1985},
publisher = {ACM Press},
pages = {252262},
note = {Providence, R.I.} } 
[article] bibtexE. R. Olderog, "Correctness of Programs with Pascallike Procedures without Global Variables," Theoretical Computer Science, vol. 30, pp. 4990, 1984.
@article{ol84,
author = {E.R. Olderog},
title = {Correctness of Programs with {P}ascallike Procedures without Global Variables},
journal = {Theoretical Computer Science},
year = {1984},
volume = {30},
pages = {4990} } 
[inproceedings] bibtexE. R. Olderog, "Hoare's logic for programs with procedureswhat has been achieved?," in Proc. Proc. Logics of Programs, 1984, pp. 383395.
@inproceedings{ol84overview,
author = {E.R. Olderog},
title = {Hoare's logic for programs with procedureswhat has been achieved?},
booktitle = {Proc. Logics of Programs},
editor = {E.M. Clarke and D. Kozen},
volume = {164},
series = {Lecture Notes in Computer Science},
year = {1984},
publisher = {Springer},
pages = {383395} } 
[article] bibtexK. R. Apt and E. R. Olderog, "Proof Rules and Transformations Dealing with Fairness," Science of Computer Programming, vol. 3, pp. 65100, 1983.
@article{ao83,
author = {K.R. Apt and E.R. Olderog},
title = {Proof Rules and Transformations Dealing with Fairness},
journal = {Science of Computer Programming},
year = {1983},
volume = {3},
pages = {65100} } 
[article] bibtexE. R. Olderog, "On the Notion of Expressiveness and the Rule of Adaptation," Theoretical Computer Science, vol. 24, pp. 337347, 1983.
@article{ol83,
author = {E.R. Olderog},
title = {On the Notion of Expressiveness and the Rule of Adaptation},
journal = {Theoretical Computer Science},
year = {1983},
volume = {24},
pages = {337347} } 
[inproceedings] bibtexE. R. Olderog, "A Characterization of Hoare's logic for programs with Pascallike procedures," in Proc. Proc.~15th ACM Symp.~on Theory of Computing, 1983, pp. 320329.
@inproceedings{ol83phd,
author = {E.R. Olderog},
title = {A Characterization of {H}oare's logic for programs with {P}ascallike procedures},
booktitle = {Proc.~15th ACM Symp.~on Theory of Computing},
year = {1983},
publisher = {ACM Press},
month = {April},
pages = {320329},
note = {Boston, Mass.} } 
[article] bibtexE. R. Olderog, "Sound and Complete Hoarelike Calculi based on Copy Rules," Acta Informatica, vol. 16, pp. 161197, 1981.
@article{ol81msc,
author = {E.R. Olderog},
title = {Sound and Complete {H}oarelike Calculi based on Copy Rules},
journal = {Acta Informatica},
year = {1981},
volume = {16},
pages = {161197} } 
[inproceedings] bibtexH. Langmaack and E. R. Olderog, "Presentday Hoarelike systems for programming languages with procedures: power, limits and most likely extensions," in Proc. Automata, Languages and Programming (Proc.~7th ICALP), 1980, pp. 363373.
@inproceedings{lo80l4,
author = {H. Langmaack and E.R. Olderog},
title = {Presentday {H}oarelike systems for programming languages with procedures: power, limits and most likely extensions},
booktitle = {Automata, Languages and Programming (Proc.~7th ICALP)},
editor = {J.W. de Bakker and J. van Leeuwen},
volume = {85},
series = {Lecture Notes in Computer Science},
year = {1980},
publisher = {Springer},
pages = {363373} }